AxiomMath formalizes the Classification of Finite Simple Groups in Lean, 43.1M lines checked by the kernel

43.1M lines of Lean. Holy shit.

Sure, but is any of that going to be mathematically useful?

Pretty sure it's the longest Lean proof by a wide margin either way.

This is exactly what auto-formalization is good for. Mathematicians have thought the classification was finished before and turned out to be wrong about a missing case.

They didn't miss a sporadic group. The real gap was the quasithin case, which sat in a 600-page unpublished manuscript that turned out to be incomplete.

Could you just point a frontier model at every math textbook and convert all the proofs to Lean once and for all? I keep thinking of Lean as a programming language for math.

Go write a few proofs in it and then come back to me.

The problem is that basic concepts have a dozen equivalent formulations and a human has to choose which one goes in the library. You can add five variants, not everything under the sun.

I'm at Axiom and that's close to what we actually did. A swarm of agents went through 500+ articles and books, and the hard part was stitching it together, since the same informal concept gets formalized in slightly different and incompatible ways.

People assume the result ends up unusable by humans without a ton of hand-holding. Maybe that's wrong and someone should just try it.

With enough compute, probably, but formalizing doesn't automatically give you a reusable library. There's a good xenaproject writeup on that.

Heads up, the page hijacks your back button. Open it in a new tab.

LLM formalization isn't as valuable as human formalization, but it's nice to know the Classification is actually correct.

I'm surprised they only found one gap. I'd have expected a bunch of fixable gaps, given how many papers by how many people this is spread across.

Loads of gaps were found and patched by humans over the last forty years. Their blog says 34 noteworthy deviations from the published record had to be resolved, the biggest one being the Unbalanced Group Theorem.

Filling in known gaps like this is what the AI labs should be spending compute on, not scooping research that's already in progress.

Looking at the proof map visualizations, I wonder whether the embeddings themselves could suggest results, assuming the embeddings are any good.

Groups were my gateway into abstract algebra. Frontier models are decent at linking the abstract definitions to plain English examples, so it's a better time than ever to pick it up solo.

The classification makes me uneasy as a mathematician, though I suppose this helps. Go read about the Monster group and then monstrous moonshine.

Shame the homotopy type theory crowd never got their act together. Formalization is so mature now and it's still done on set-theoretic foundations.

Lean isn't set theory, it's type theory, and translating a type-theoretic formulation to HoTT is fairly easy. We're making steady progress, see the cubical-bis table.

I blew my whole Claude Max weekly budget having Opus translate Mathlib to Coq-HoTT last week. It was beautiful, I'm doing it again this week.

What a monster of an effort.