Hacker News Reader

Jblx2on A Beginning for Mathematics

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

Jblx2on A beginning for mathematics

Not the OP, but how about things like:

https://ciechanow.ski/archives/

...for starters?

Jblx2on A beginning for mathematics

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

Jblx2on A beginning for mathematics

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.

Jblx2on A beginning for mathematics

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

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

Jblx2on Iran's Internet Blackout Is Almost Impossible to Escape

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.

Jblx2on OpenAI’s Navier-Stokes release included a Lean 4 formal proof

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

Jblx2on OpenAI’s Navier-Stokes release included a Lean 4 formal proof

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

Jblx2on OpenAI’s Navier-Stokes release included a Lean 4 formal proof

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?

Jblx2on AI Doomlord Jacob Coxon's Media Tour Has Begun

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?

Jblx2on The Nonfiction Book Market is Collapsing?

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.

Jblx2on I resigned from Anthropic today

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

Jblx2on The Nonfiction Book Market is Collapsing?

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.

Jblx2on Tao: Open math problems being non-renewably mined by AI

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 other AI labs as well.

Jblx2on Mercury 2.5

Not related to the Mercury language:

https://mercurylang.org/

Jblx2on On the Navier–Stokes Millennium Prize Problem

https://ammkrn.github.io/type_checking_in_lean4/trust/trust....

Jblx2on On the Navier–Stokes Millennium Prize Problem

>A proof is not like a program.

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

Jblx2on Tao: Open math problems being non-renewably mined by AI

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

Jblx2on Schemy Lisp En DOS

How much does that really get used?

Jblx2on Fermat's Last Theorem in Lean 4

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

Jblx2on Formalizing Fermat's Last Theorem

Not mm0?

Jblx2on Formalizing Fermat's Last Theorem

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

Jblx2on Formalizing Fermat's Last Theorem

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/type_checking_in_lean4/title_page.h...

...and some thoughts on putting stuff in the kernel:

https://lawrencecpaulson.github.io/2026/07/30/Collatz.html

Jblx2on Formalizing Fermat's Last Theorem

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

Jblx2on True Rate of Unemployment

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

Jblx2on How accurate have Ed Zitron's AI skeptic predictions been?

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

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

Jblx2on I keep getting flagged for AI, but I suck at writing. How can I solve this?

Ah, the royal road to learning how to write.

Jblx2on The turbulent AI era is here. The choices we make now are critical

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?

Jblx2on Everyone says assembly is untyped—everyone is wrong

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

Jblx2on U.S. preparing to force Netherlands to ban ASML from selling to China

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?