Jblx2

6 ms·

1.
by Jblx2 4d ago
PWDR. Why doesn't satellite get around whatever blocks Iran has in place? Are they able to effectively able to jam everything? Seems like the U.S. should be paying the satellite providers to give away "free" service in Ira
2.
by Jblx2 6d ago
People also need to be cautious with potential adversarial proofs. Like don't decide to give money on a sure-bet thing, just because they have a Lean proof. Not saying that these AI labs would do this. a^n ＋ b^n ＝ c＾ｎ ...(there are t
3.
by Jblx2 6d ago
In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean&
4.
by Jblx2 6d ago
What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?
5.
by Jblx2 6d ago
Kind of odd that I haven't seen him mentioned in any of these discussions. How does Ted Kaczynski fit into all of this? * He was correct * He was wrong * He was correct, but for the wrong reasons * He was correct, but too ex
6.
by Jblx2 7d ago
Why would that be the case? Fiction books are already imaginary, so it makes less of a difference whether it is human-imaginary or reshuffled-by-LLM-imaginary. Non-fiction I expect to not be hallucinated-out-of-the-ether.
7.
by Jblx2 7d ago
>In 1900, there was no evidence of the kind you seek that lighter [sic]-than-air flight was possible. Presumably you meant heavier than air? Also, I'm pretty sure that birds existed in the years leading up to 1900.
8.
by Jblx2 8d ago
I started reading and at about the half-way point, I decided to search for "AI", "LLM", "generative", which all came up blank. At that point I closed the tab and headed back here. #1 reason I would be very sk
9.
by Jblx2 8d ago
OpenAI has already said they aren't going to claim the $1,000,000. If this proof claim holds up, then the Millennium prizes will be 2 for 2 for rejections of the prize money for valid solutions. Maybe that will be the precedent for o
10.
by Jblx2 8d ago
Not related to the Mercury language: https://mercurylang.org/
11.
by Jblx2 8d ago
https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
12.
by Jblx2 8d ago
>A proof is not like a program. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
13.
by Jblx2 8d ago
Obviously, he was trying to avoid being labeled as a crank for working on a famous problem like that for so long.
14.
by Jblx2 9d ago
How much does that really get used?
15.
by Jblx2 11d ago
You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean. https://arxiv.org/html/2403.14064v3 https://github.com/dig
16.
by Jblx2 12d ago
Not mm0?
17.
by Jblx2 12d ago
How about all of these bugs from last week? https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t... ...I'm not saying this FLT result is compromised. I suppose things depend on your perspective where we
18.
by Jblx2 12d ago
the Nanoda type-checker for Lean is ~5,000 lines of Rust: https://leodemoura.github.io/blog/2026-3-16-who-watches-the-... ...and for those who are looking to roll-their-own: https://ammkrn.github.io/typ
19.
by Jblx2 12d ago
You still have to trust that the AI didn't exploit a bug in the Lean kernel. There was just such an instance of a bug a little over a month ago: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
20.
by Jblx2 15d ago
If you do this with PPP with every other country on earth, which ones look the best?
21.
by Jblx2 15d ago
I think you missed a "I won't respond further." https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
22.
by Jblx2 21d ago
Ah, the royal road to learning how to write.
23.
by Jblx2 21d ago
How would that work? Make a law that it is illegal to own more than X GFLOPS of computing per person? With another limit on corporations? Maybe a Computing Enforcement Agency to investigate potential violations? On a slightly different
24.
by Jblx2 26d ago
Can you get an assemble-time or run-time type-error with assembly? Might be a fine article otherwise without the click-bait headline.
25.
by Jblx2 27d ago
How much profit would ASML lose to this ban? Maybe they'll get a couple hundred million dollars in annual compensation from the U.S. gov?
26.
by Jblx2 28d ago
Apparently, it is Palomar: https://terrytao.wordpress.com/2026/08/18/palomar-a-registry...
27.
by Jblx2 28d ago
Are dolphins obsolete?
28.
by Jblx2 28d ago
Yes, you still need to be careful, especially if you have reason to think that the proof was from a malicious actor. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... (N.B. from August 2026)
29.
by Jblx2 28d ago
It will be interesting to see the evolution of journals in the next ten years for sure. Have they outlived their usefulness? Maybe everyone will just upload papers to arXiv, along with a copy of the formal proof.
30.
by Jblx2 28d ago
Mochizuki enters the chat

More ›