Ahmad Rammal and Meta AI release ATLAS, translating 25 textbooks into 500,000 lines of Lean 4

500k lines of code, but the statements are just wrong or excessively simplified…

Thanks to Christian Merten and Jack McCarthy for looking at this in detail on Zulip (link below). Note for example that their definition of a compact orientable manifold is "a compact manifold" 😂

We did it! Thrilled to announce that with my team at FAIR Meta we released 25+ auto-formalized mathematics textbooks covering analysis, algebra, geometry, topology, combinatorics, probability, statistics, PDEs, number theory, and theoretical computer science - the largest such effort to date.

Here's a "theorem" in the complex variables section proved by sorry: "If g is complex differentiable at every point with Re z \geq 0, then g is complex differentiable everywhere." This is then used in the proof of another theorem in Lecture21.lean. All of this is marked as a "pass".

Very interesting work here! Lots of rough edges (misformalizations, etc) but it points the way to a landscape of possibility!

What will be really interesting is to see if it's possible to actually teach out of such books (and of course clean things up as you go)... [It's possible that the AI took so many shortcuts that it really doesn't represent the difficulty of some proof, etc; still, experiments like these can give a lot of useful information.]

See https://leanprover.zulipchat.com/#narrow/channel/583336-Autoformalization/topic/Atlas.20.28Meta.29/near/598359219 and https://leanprover.zulipchat.com/#narrow/channel/583336-Autoformalization/topic/Atlas.20.28Meta.29/near/598435363

@sujeetbhlr @littmath Actually super happy to find my timeline filled with people dunking on this

@KempeLab It might be best to be more precise. The whole post reads as though you actually formalized 25+ books, but a quick check shows that you formalized material from open courses. That is good enough, it’s just not 25+ books. That's why the original post mentioned "from".

@arnal_charles @AIatMeta All such efforts are awesome, congrats! Two remarks:

- you could use Codex which is much better at math than Opus - check out our open source harness which might help with verification/formalization: https://github.com/ulamai/ulamai

@Someody42 I just don't understand. The whole appeal of Lean (to this crowd) is making it easier to "trust" model output, but having models be the enforcers of the remaining burden of trust seems to defeat the idea

Amazing!

@sujeetbhlr A useful theorem indeed !

ATLAS was generated with our AutoformBot harness, with zero manual proof engineering.

AutoformBot: https://github.com/facebookresearch/autoform-bot

AutoformBot is compatible with frontier model APIs and coordinates multiple LLM agents acting as orchestrators, workers, and reviewers. It can leverage substantial parallelism within each formalization attempt, reducing wall-clock time. (6/9)

@KempeLab @TacoCohen We need this for every possible domain to make colleges obsolete. We need more autodidacts and polymaths.

@sujeetbhlr @littmath Ok, but if this attempt of formalization is serious (which I assume) then all sorry-statement needs to get removed anyway and those problems should naturally surface. Good to reveal such holes early, but it does not contradict the goal, doesn‘t it? Can get better!

@DocOctagonical @AIatMeta For now, we have mostly focused on textbook-like lecture notes from MIT for convenience: they are openly available, well structured, and cover a broad range of topics. We plan to extend beyond these sources in the near future.

@Someody42 @ElliotGlazer I saw sorrys in less than 30s of clicking this announcement and stopped there. Why announce it half baked but not say so?

@robin_stammer @sujeetbhlr @littmath the problem is not that it's a sorry statement, it's that it's blatantly false