231–240 of 526 posts
There's a wonderful documentary by BBC Horizon with Andrew Wiles from 1996 – highly recommend! I saw it in the 90's and it's a documentary for everyone. It captures the effort, struggle, highs and lows of a 7 year effort working on Fermat's Last Theorem.
Earlier quoted context omitted.
my messages are so gloomy because i am heartbroken, that given a technological miracle again, we could snatch tragedy from the jaws of our emancipation. will you not see that people could be truly empowered and yet will instead be oppressed?
So oppressed that they are one of the main reasons for positive gdp growth in the USA, tax revenues, mathematical/scientific innovations etc. They're doing all this but still can't imagine a positive vision for the world but be a doomer. What a sad state the world is in, the humans are more prosperous, healthier than ever but looks like the seven deadly sins might never go away.
that is not formally valid. in between those two you are smuggling the assumption that gdp growth, tax revenues and scientific innovations are good.
a) those metrics are poisoned, per Goodheart's law.
b) they are not good and human welfare will get worse as gdp, tax revenues and innovations grow.
i leave b for the reader to complete.
An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable. I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think…
"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…
Wiles-Taylor-Wiles was the original proof by Andrew Wiles, and its corrections.
Galois representations is about vectors over Galois extensions, which are essentially adding roots to regular numbers (rationals, integers, etc). That ties into the Langlands program, which is a big area in number theory (that I don’t know much about).
Together with flat deformations and Frey curve, I think they’re talking about a topic in algebraic geometry as applied to number theory.
I also recognize the name Eisenstein from my time as an undergrad, though two decades out and not working in the field I’ve forgotten what his work on ideals implied here. Ideals are a well-known topic though, a sort of structure inside a ring (set with + and *) that is closed under operations — like evens in the integers are the 2Z ideal.
So I’d describe it as “sensible with an undergrad background”.
"The proof is not the modern proof which I have been formalizing myself following ideas of Khare, Taylor etc, but the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet’s level-lowering theorem. Anthropic’s repository develops Fontaine theory (to study flat deformations of Galois representations) and develops enough of Mazur’s work on the Eisenst…
Vaguely. It's describing connections between a number of other mathematics results than can be connected to prove FLT. I assume all the work described is being done to make the proof more presentable, smaller, basically "prettier".
It sounds like they established a minimum and maximum bounds for n in x^n + y^n = z^n, where one proof works for n greater than or equal to 17, and another proof for n I believe the case (remembering back 40 years here) n is even is very easy, and n is composite and odd slightly less so. Neither really being in the ballpark of what they describe here.
Earlier quoted context omitted.
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless. You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itse…
> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic. Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
Earlier quoted context omitted.
> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic. Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.
Earlier quoted context omitted.
Do you have proof of this bug or something? Is this just envy against computers now ?
as mentioned elsewhere, there was a bug in the lean kernel exploited by AI to prove a false statement roughly a month ago https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
Earlier quoted context omitted.
A human definitely didn't, but one of the benefits of formal verification is that even if the work done to achieve something is slop-y or excessively verbose, solvers like Lean guarantee that the initial proposition (assuming it was written correctly and in this case was definitely reviewed by humans) is definitively True. This is true across other domains of formal verification outside of math as well
guaranteed, up to lean itself having bugs that are exploited by the LLM :shrug:
Earlier quoted context omitted.
If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.
support your point with explanation or be ignored :-)