Jblx2

3 ms·

1.
by Jblx2 11d ago
Does anyone have a rough estimate of how many research mathematicians there are in the U.S. or world?
2.
by Jblx2 12d ago
Not the OP, but how about things like: https://ciechanow.ski/archives/ ...for starters?
3.
by Jblx2 12d ago
>Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. Do any one person even understand the humble pencil? https://dn790006.ca.archive.org/0/items/
4.
by Jblx2 12d ago
That seems like a red herring. Have you independently verified the human generated proof of FLT? Surely someone else will try to verify Anthropic's formalization on different hardware. Plus, it seems likely that FLT formalizations w
5.
by Jblx2 12d ago
Kind of makes me think of Arnold's, "On Teaching Mathematics": https://www.maths.tcd.ie/pub/Maths/Courseware/ProblemSolving...
6.
by Jblx2 13d 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
7.
by Jblx2 15d 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
8.
by Jblx2 15d 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&
9.
by Jblx2 16d 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?
10.
by Jblx2 16d 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
11.
by Jblx2 17d 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.
12.
by Jblx2 17d 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.
13.
by Jblx2 17d 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
14.
by Jblx2 17d 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
15.
by Jblx2 17d ago
Not related to the Mercury language: https://mercurylang.org/
16.
by Jblx2 17d ago
https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
17.
by Jblx2 17d ago
>A proof is not like a program. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
18.
by Jblx2 17d ago
Obviously, he was trying to avoid being labeled as a crank for working on a famous problem like that for so long.
19.
by Jblx2 18d ago
How much does that really get used?
20.
by Jblx2 21d 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
21.
by Jblx2 21d ago
Not mm0?
22.
by Jblx2 21d 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
23.
by Jblx2 22d 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
24.
by Jblx2 22d 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...
25.
by Jblx2 24d ago
If you do this with PPP with every other country on earth, which ones look the best?
26.
by Jblx2 24d ago
I think you missed a "I won't respond further." https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
27.
by Jblx2 1mo ago
Ah, the royal road to learning how to write.
28.
by Jblx2 1mo 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
29.
by Jblx2 1mo 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.
30.
by Jblx2 1mo 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?

More ›