Jblx2

Does anyone have a rough estimate of how many research mathematicians there are in the U.S. or world?

Not the OP, but how about things like:

https://ciechanow.ski/archives/

...for starters?

>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/i-pencil-pdf-2019/I%...

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 will improve / get shorter over time, requiring less compute. And computers (and type-checkers) will continue to get faster over time as well. So maybe in 5 years you could own a computer fast enough to verify a/the proof in say a week, instead of 5 hours.

Kind of makes me think of Arnold's, "On Teaching Mathematics":

https://www.maths.tcd.ie/pub/Maths/Courseware/ProblemSolving...

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 Iran. Maybe there are just not enough receivers and they are too expensive? Plus, maybe a summary execution if caught with a receiver. Maybe the U.S. should be doing air drops of satellite receivers.

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 two different "n"s in the above https://unicodeplus.com/U+FF4E . In addition, the plus sign is: https://unicodeplus.com/U+FF0B . I tried to use another "n" as well: https://unicodeplus.com/U+1D5C7, but looks like HN strips it out, even though it looks identical to the ASCII "n" in the default font on my browser.)

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", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean").

https://github.com/openai/NavierStokesAndEuler/blob/main/Nav...

?

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?

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 extreme 
  * He was correct, and not extreme enough
  * He was correct, but too early
  * He was correct, but unpleasant as a person 
  * I haven't read the manifesto, but I have strong opinions anyway
  * Ted who?

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.

>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.

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 skeptical of purchasing a book published in 2026 is AI. Unfortunately, you need to overcome a pretty big hump in convincing me that there was no AI involved in authoring.

OpenAI has already said they aren't going to claim the $1,000,000. If this proof claim holds up, then the Millennial prizes will be 2 for 2 for rejections of the prize money for valid solutions. Maybe that will be the precedent for other AI labs as well.

Not related to the Mercury language:

https://mercurylang.org/

>A proof is not like a program.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Obviously, he was trying to avoid being labeled as a crank for working on a famous problem like that for so long.

How much does that really get used?

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/digama0/lean4lean/tree/master

Not mm0?

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 are on the spectrum of "finding more bugs means there are fewer left to discover" vs. "finding more bugs probably means there are still unexplored corners out there".

the Nanoda type-checker for Lean is ~5,000 lines of Rust:

https://leodemoura.github.io/blog/2026-3-16-who-watches-the-...

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...

If you do this with PPP with every other country on earth, which ones look the best?

I think you missed a "I won't respond further."

https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...

Ah, the royal road to learning how to write.

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 topic, why have I never heard about taxes for AI/robots? Is there a reason why people should be the only taxpayers?

Can you get an assemble-time or run-time type-error with assembly? Might be a fine article otherwise without the click-bait headline.

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?