Classification of Finite Simple Groups Formalized in Lean

243 pointsposted 4 days ago
by pfdietz
(cfsg.axiommath.ai)

85 Comments

mlmonkey

4 days ago

Out of curiosity: is it possible to take a frontier model and just let it loose on all math textbooks out there, converting each and every proof/theorem/lemma/etc. into Lean? A frontier model should be able to do that, right? And it's a one-time task: do it once and it's there for eternity, available as a library to be used in other proofs.

Maybe my understanding of Lean is wrong; I'm thinking of it as a programming language but for Math.

jonath_laurent

4 days ago

Axiom MTS here. What you describe is pretty close to how we formalised this proof, which is scattered across more than 500 articles and books: a swarm of agents was tasked with going through all these sources.

One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.

petesergeant

3 days ago

As someone with a highly uneven and kinda basic maths background, I'd have thought that simplification of a proof, and pulling things into a coherent whole would be exactly what computers excel at, but everything I've seen (or heard) suggests that's not really the case. Are you able to explain why?

seanhunter

3 days ago

There are some (typically small) simplifications that computers are indeed good at. These could be thought of as analogous to compiler optimizations - they’ll see that your proof is basically composing several lemmas and that some of the work in the middle can be removed so it can just do that. In many cases with lean if you post a short to medium-length proof into an llm it can suggest these types of small improvements for you.

What they’re not that great at is the type of improvements that really make a big difference: big simplifications etc. This is not super suprising when you understand how this works.

Firstly proofs in lean (and I think many other assistants) are essentially functions which take hypotheses and instantiate a particular type. That type being equivalent (due to the Curry-Howard correspondence) to a proof of some proposition. The assistant uses dependent type theory to make sure all the types match up at each step, which is what makes it rigorous. So the task of simplifying a proof is basically finding a route through an infinite-dimensional space where you know your starting location and the desired end point, but at any step you can go in basically any direction you like so long as you can justify your step. You justify a step by either choosing from a (vast at this point) library of lemmas and theorems that are in your standard library, or by recursively building the proof/function you need to justify the step you want to take using this same process you’re trying to use for simplification. This is incredibly flexible, but means you’re actually spoiled for choice and planning is hard.

Secondly, in “pen and paper” proofs, LLMs don’t know the difference between steps which are important/easy/hard/intuitive/non-intuitive for human mathematicians, so lots of the proofs they produce are extremely clunky and pedantic in places and dwell for ages over details that are obvious and would usually be skipped over and then will move very fast through things that justify more attention. This unevenness is part of what makes their proofs hard for humans to work through, but also means they are generally poor judges of what would actually constitute a decent simplification.

fspeech

3 days ago

Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.

josh-wrale

3 days ago

Maybe there will be an OpenAPI or gRPC of proofs to solve this to some extent, or maybe lean4 is already that, ig.

nextaccountic

2 days ago

Uhm three ideas about that (they don't solve the problem on their own, they just show mathematicians care about this issue)

Category theory can be viewed as a framework to make math more modular and compatible. For example topos theory can be used to transport definitions to other "mathematical universes" of sorts

Another point of view is that is working with synthetic mathematics which is a bit like "programming" mathematics with an abstract API. The opposite, analytic mathematics, leak implementation details (for example, the von Neumann construction of natural numbers, which is analytic, leak the implementation detail that 0 is defined as the empty set; but the peano axioms are synthetic and doesn't leak any such details)

There is also the principle that two mathematical objects that are isomorphic (have the same structure) are actually the same thing. For example if you construct the natural numbers two different ways, they are "the same thing" in a sense. This usually is stated informally, but a rigorous formulation of that is the univalent principle

gus_massa

3 days ago

A few unrelated examples:

Some books assume 0 is Natural but other start from 1.

In some books all Rings https://en.wikipedia.org/wiki/Ring_(mathematics) have a multiplicative identity. Almost all books assume Algebras have an identity, but there may be weird cases.

Some books say in the first page that they will assume all groups are Abelian/Commutative, and not repeat the assumption in each page.

There are like 8 conventions to define the Fourier Transform. All are equivalent, but each one add different constants here and there. Beware to combine formulas from different books.

I guess it's easier for the computer to track the details and remember to translate the names in each book article to a consistent set of definitions.

hujun236

3 days ago

When two sources formalized the same object in incompatible ways, did the swarm mostly emit translation lemmas between them, or did someone pick a canonical definition and have downstream proofs rewritten to match? The second feels like where the "coherent whole" cost actually sits, and I'm curious how much of the 500-source effort was that reconciliation versus line-by-line translation.

p11p

4 days ago

[flagged]

penteract

4 days ago

Producing a formalized proof from a non-formalized proof in a paper or book should not be considered a violation of copyright.

pfdietz

4 days ago

Indeed; one cannot copyright mathematical ideas, only their specific expressions. And the formalization is a different expression.

bananaflag

4 days ago

Yes, but thing is, for a lot of basic stuff there are myriad ways in which it is formulated, so humans have to decide which of them goes in the library. Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.

Probably this will be done in some form in the coming months.

xelxebar

3 days ago

The really interesting aspect of this, IMHO, is discovering what theorem formulations combine together well as a whole. It's much akin to a software architecture problem.

Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.

One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.

thaumasiotes

4 days ago

> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.

Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).

Someone

4 days ago

_If_ you have formalized a provable theorem in Lean, a simple bread-first search can prove it. It will take lots (and lots, and lots, and lots…) of time, though (https://en.wikipedia.org/wiki/General_Problem_Solver).

LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.

user

4 days ago

[deleted]

QuesnayJr

4 days ago

I think people assume that it would end up not being usable by humans without a lot of hand-holding. Though maybe that's wrong, and somebody should try it.

tyromaniac

4 days ago

Write a few proofs with it and then come back to this

SwtCyber

3 days ago

I think you're basically right about the end goal yet the gap between a textbook proof and a Lean proof is much bigger than it looks

sebzim4500

4 days ago

This seems like a very good use of auto-formalization, because in the past mathematicians have incorrectly believed that they were finished with the classification only discover a missing class/sporadic group.

The original proof was a collaboration of ~100 mathematicians, if Tao is correct then we should expect to see more such collaborations in the future like we do in e.g. physics.

QuesnayJr

4 days ago

They didn't discover a missing sporadic group. The big gap in the proof (the quasithin case) happened because it was covered in a 600-page unpublished manuscript that under further investigation turned out to be incomplete.

SwtCyber

3 days ago

And what's interesting is that formalization doesn't just catch missing cases, it also forces you to examine all the assumptions that everyone has been taking for granted

compacct27

4 days ago

Groups were my gateway drug into abstract algebra. A friend clued me into symmetry being everywhere and Groups are how symmetry is formalized, and it’s been a crazy journey understanding all that. The frontier models can tie those abstract concepts to plain English examples and answer questions decently well, it’s never been a better time to pick up the field solo and see what it has to offer us

ykonstant

3 days ago

This is phenomenal, super important for me. I have always had my concerns about the classification, and the verification that such a monumental proof is correct gives me great confidence about the way we have been doing mathematics so far.

Davidzheng

4 days ago

Makes me sad that the homotopical foundation people never got their shit together and now formalization is so mature but it's still done in set theoretic foundations.

abstractanimal

3 days ago

Last week I blew my whole Claude Max weekly budget having Opus translate from Mathlib to Coq-HoTT. It was so beautiful I can't wait to do it again this week.

HappyPanacea

4 days ago

The stronger AI become the easier it should be to develop and move to alternative foundations.

Ericson2314

3 days ago

No Type Theory won: Per Martin-Löf is still alive and should be able to confirm his work lives in some form in Lean. Zermelo and Fraenkel would be utterly confused, however.

What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).

I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.

semolinapudding

3 days ago

Im' not sure he'd say that -- Per Martin-Löf's original work was to develop a computational and predicative foundation for constructive mathematics à la Bishop.

Lean's type theory kinda gives up on that idea: Mathlib gleefully postulates impredicative propositions with the axiom of choice, quotient types, etc. All in all, I'd say that Lean is much closer in spirit to De Bruijn's AUTOMATH project (which pre-dates Martin-Löf!), whose goal was to formalise classical math textbooks using dependent types.

Ericson2314

3 days ago

I am saying that Martin-Löf would see his work in Lean, not mathlib. Mathlib is a library. In Lean you can "contain" classic reasoning to certain parts of the code base, and that is also true in the original MLTT: you can postulate classical axioms as functions in scope.

semolinapudding

2 days ago

Even without Mathlib, Lean's type theory is impredicative. Martin-Löf does not consider impredicativity to be constructive.

anon291

3 days ago

Hey now... If you have a formulation in type theory (lean is not set theory), then you can translate to homotopy type theory fairly easily

QuesnayJr

4 days ago

I'm surprised they only found one gap. I would have expected multiple (fixable) gaps would have been uncovered, especially since the result was spread over many papers by many different people.

contubernio

4 days ago

Many many gaps had been found and patched (by humans) already over the last forty years.

pfdietz

4 days ago

The formalization is 43.1M lines of Lean.

cubefox

4 days ago

I suppose this is the longest Lean proof by a wide margin.

pfdietz

4 days ago

It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux).

cubefox

4 days ago

I wonder whether humans could have realistically finished it without AI by 2100.

cvoss

4 days ago

I would bet no. Because the original proof is so distributed, with parts of it being very old, and with parts of it being, as a first attempt, not the most concise or lucid route to the result, we were rapidly approaching a world where the empirical knowledge of how/why the result holds was literally dying.

The article refers to its use of the "first-generation proof". It would seem this proof is too large to be truly known by one person, and the group of people who "collectively knew" it grew old and started to die. Since its original formulation, mathematicians began to compile, consolidate, and revise the proof into a 2nd generation digested form (estimated to be 5000 pages instead of tens of thousands). But that effort was still so monumental in its own right that a 3rd gen proof project began to digest the 2nd gen proof before the 2nd gen proof was even finished. I believe both the 2nd and 3rd gen projects are still ongoing.

It will be interesting to see how small the proof gets once we finish learning how to obtain these results "efficiently" with the benefit of hindsight.

sebzim4500

4 days ago

Depends if you include a few decades of improvements in lean itself. Non-AI proof automation is much better than it was even a year ago and so some fiddly results can now be done with `by grind`.

Also don't discount the fact that people would learn how to do this kind of project, currently no one really knows how to decide what definitions work best, what should be reducible, what should be part of a public api and what should be local to a module, etc.

mrguyorama

3 days ago

Would we have been allowed to dedicate $2 trillion dollars to mathematicians doing this?

bwestergard

4 days ago

Is that going to be mathematically useful?

sebzim4500

4 days ago

It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.

cvoss

4 days ago

Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.

Panoramix

4 days ago

How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.

kenferry

4 days ago

Well, the point of the _computer_ formalization is that it's checkable.

An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.

adrianN

3 days ago

An error in the formalization could also be that you formally prove something different from what you think you proved.

pfdietz

3 days ago

All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.

This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.

sebzim4500

4 days ago

In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.

In this case the statement is unusually complicated but still much much easier to verify than the proof itself.

CJefferson

3 days ago

So, the specification of the theorem we are fairly solid on, formalising what a group is, and a simple group, have been done a long time and we are confident in the correctness of.

Assuming you do trust those, then assuming the formalisation passes lean (and lean has no bugs!), then the whole idea is you've got a proof of the theorem.

anon291

3 days ago

The papers describing lean and it's core operations are deliberately small. The kernel of a theorem prover is meant to be such that a human can check it for correctness. The kernel does not include things like type inference or execution. It literally checks the proof and that's all and everything needs to match exactly. It's fairly trivial to write such a thing.

Humans have to establish trust in this.

After that, the rest of the language is written. Yes it is possible the type inference engine is broken but in that case the kernel will reject it

pfdietz

4 days ago

The proof was of such complexity and length there were lingering doubts. This dispels them.

user

4 days ago

[deleted]

curt15

4 days ago

More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.

claudismusa

4 days ago

I used to take mathematicians seriously.

pfdietz

3 days ago

What do you mean by that?

user

3 days ago

[deleted]

senderista

4 days ago

Filling in well-known gaps like this is the kind of thing the AI companies should be doing, not trying to scoop research in progress.

pixl97

4 days ago

Page has some kind of redirect bug that steals the back button, may want to open it in a new tab to avoid that.

vatsachak

4 days ago

LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct

pred_

3 days ago

What did it cost and how much energy was spent?

vessenes

4 days ago

Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.

sashank_1509

3 days ago

I’m not sure what axiom maths business model is, seems like excesses of AI boom era.

No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.

nilkn

a day ago

Autonomous software and hardware verification. They're just getting started. It's not just Axiom: Logical Intelligence, Harmonic, and a new one that just launched (&Truth). I suspect the business case is addressing the global cybersecurity crisis that AI is creating.

Making it cheap to do is probably exactly what they're trying to do. Formal proofs for verification take 10-20x as many lines as the core functional code being verified. Nobody's going to want to pay for 10-20x as many tokens at frontier pricing for verification unless they have to or it yields tremendous benefits. So getting the token price down as low as possible for a prover is probably a core part of the value proposition.

namibj

2 days ago

What proofs are good for is decoupling implementation and semantic definition of software (and application specific circuits).

Like, proving that in the absence of hardware faults, some optimizer for JavaScript can never result in arbitrary memory accesses.

Or that some database doesn't violate data semantics under ANY condition.

Or that as long as not too many sensors fail, a plane autopilot will not go and do anything that would lead the plane to exceed safe speeds and forces/accelerations. (Won't just go crash the plane or drop it from the sky in one or more pieces just because some few sensors froze or caught lightning or something.)

nwah1

3 days ago

Simplifying and composing these proofs with other proofs should probably be the next goal. And formalizing within other computational proof paradigms.

richard_chase

3 days ago

I was thinking this would be done at some point but not so soon.

esafak

4 days ago

Looking at the visualizations made me wonder if the embeddings themselves can be used to suggest, if not derive, mathematical results. I realize it depends on the quality of the embeddings.

gdiamos

3 days ago

This tech is about to come for software.

user

4 days ago

[deleted]

xiaodai

3 days ago

what a monster of an effort!

sdenton4

3 days ago

i_see_what_you_did_there.gif

user

4 days ago

[deleted]

Salparvezml

4 days ago

The counterexamples to a closure step in one of the published routes are the strongest case for doing this. A proof treated as settled for decades still had a hole, and it took a machine-checkable record to surface it. I'd like to know how many of the 500 sources needed a repair rather than just a translation.

v3ai

4 days ago

based if true