Earlier quoted context omitted.
ok, you now added some unknown inference system in addition to zfc
No, it is the same inference system. They are just abbreviations.
and what is that system?
Formalizing Fermat's Last Theorem
491–500 of 537 posts
Re: Formalizing Fermat's Last Theorem
#492Earlier quoted context omitted.
The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main...
I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
Re: Formalizing Fermat's Last Theorem
#493Earlier quoted context omitted.
Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
The token price seems like a poor measure. Building the LLM that could do this work in 11 days cost multi billions. The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept. Otherwise this cost a lot more than we’d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.
Human mathematicians also have to eat right, trained, etc.
Re: Formalizing Fermat's Last Theorem
#494Earlier quoted context omitted.
I enjoyed this Terence Tao post the other day. The relevant quote is > one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?" And later > But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided…
That seems narrow minded. Theres both "learnings directly related to the thing studied" and "learnings downstream from the thing studied". If you imagine mathematics being a huge sudoku puzzle of unknowns you are trying to fill in, each previously empty square you are able to fill in (or gain a smaller bound on) has implications in all sorts of other areas.
It's important to remember that most mathematics is not science - large parts of it are mostly esthetic pursuits that bring joy to certain mathematicians, and sometimes happen to have unexpected benefits to science or engineering (like how number theory suddenly became important to cryptography in the 20th century).
Fermat's last theorem is a great example - it is in itself a completely irrelevant observation, not used (so far) in any larger theory. It was only pursued because (a) Fermat casually claimed to have easily proved it (almost certainly being mistaken about it), and (b) it sparked the curiosity of mathematicians because it looks so simple but turned out to be so hard.
So what does humanity gain by knowing that the theorem holds? Basically nothing. What does humanity gain from the process of proving it? As far as it is known for now, basically nothing (though it is somewhat likely that the complex theories created to prove it will find other applications). However, those that have worked on it, and the guy who did prove it, gained a huge amount of personal insight into mathematics, and surely grew as mathematicians, and will hopefully use those skills in working on other problems that may prove more directly useful. Plus, they had a great time doing it.
What this means is that, if the proof had been discovered entirely by AI, basically nothing would have been gained. LLMs don't learn by doing, so no personal experience growth would have come from this; and as I mentioned, both the result and the proof are, so far, quite irrelevant even for mathematics more broadly. So it would have been actively detrimental, or at best neutral, compared to letting human mathematicians work on this problem, in a way that is never the case in science or engineering, where any bit of knowledge is in itself useful to at least some extent.
Re: Formalizing Fermat's Last Theorem
#495>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work. ^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Forgive the authors of the article for assuming readers would complete it.
you would never assume this if you've spoken to any human being, ever
Re: Formalizing Fermat's Last Theorem
#496Earlier quoted context omitted.
The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.
You don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to pe…
Interesting. Indeed, proving theorems that are stronger and more general "accidentally" than what you really need is not a bad thing.
Re: Formalizing Fermat's Last Theorem
#497Earlier quoted context omitted.
> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand. The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be tr…
But what does it matter whether we can "trust its verification of the 13 million lines of code"? We already knew that Fermat's Last Theorem is true, we don't need Lean to tell us that. The value of a formalization would be to improve our understanding of why it's true, and that can't be achieved by 13 million lines of code no human being has read. The source article does acknowledge this isn't a replacement for human…
That's a completely different matter than what this thread was about. This thread was about whether mistakes in the 13M lines of Lean code could mean that this proof could be wrong despite Lean saying it's right.
Re: Formalizing Fermat's Last Theorem
#498Earlier quoted context omitted.
>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. > Pretty insane. I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook: --- Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then H ∨ N = HN = { hn | h ∈ H, n ∈ N }. --- This says that the subgroup closure of H and N, the smallest s…
It looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.) I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".) My algebraic friends surely know it and they would never include it in a paper because everyone knows it. I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it i…
It is in mathlib. In textbooks it's presented as an introductory part of the Second Isomorphism Theorem; in mathlib it's here: https://leanprover-community.github.io/mathlib4_docs/Mathlib... .
The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup. You might call it an 'intermediate theorem' to that proof.
My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems".
In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.
Re: Formalizing Fermat's Last Theorem
#499Earlier quoted context omitted.
You make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
No, once you start formalize this, it becomes complicated. There is a reason why looks like there is no "peano can be derived from zfc" theorem which would close dispute, and my opponents need to throw links on bro math from stackexchange in this discussion.
Per https://en.wikipedia.org/wiki/Peano_axioms#Set-theoretic_mod...
> The Peano axioms can be derived from set theoretic constructions of the natural numbers and axioms of set theory such as ZF.[15]
If you're going against the general consensus you should present something more than nebulous assertions that it's wrong.
Re: Formalizing Fermat's Last Theorem
#500Earlier quoted context omitted.
I hope you keep these horrible thoughts to yourself if you ever walk through a paediatric hospital
What does a pediatric hospital have to do with aging...?
The point is that the kind of horrendous diseases you see affecting babies are also, many of them, natural parts of the human experience, just as much as aging. And yet we all like the fact that pediatric hospitals exist to cure these natural diseases.