Formalizing Chapters of Stacks Project

Stream: new members

[Jiang Jiedong]

Hi everyone,

Given that the Stacks Project is well organized and serves as a comprehensive, encyclopedic resource in commutative algebra and algebraic geometry, what do you think about organizing a group of motivated students to formalize certain sections in the Stacks Project?

There are 10-20 motivated students at Peking University, who already have some basic experience in formalizing exercises of abstract algebra. The teachers can teach them commutative algebra before they begin formalizing.

Since we are most interested in algebra, maybe beginning with "Chapter 9: Fields" is a good start and then we can try to progress towards "Chapter 10: Commutative Algebra". A (maybe stubborn) working method is to check one by one whether a theorem in the Stacks Project is already formalized in mathlib. If yes, we add the corresponding Stacks Project tag to the comments of the formal theorem (or its formal variant). If not, we try to formalize and add this theorem into Mathlib. If the theorem is too early to be formalized yet, we may leave it as a TODO.

I hold the belief that "every theorem in the stacks project should be formalized (possibly in a variant form) into Mathlib". Do you have any suggestions and comments on this project? Thank you!

[Andrew Yang]

Sounds like a good idea. The correspondence between stacks and mathlib is a nice thing to have . The Commutative algebra section is quite large though, you might want to limit the scope and focus on a selection of results.

[Ruben Van de Velde]

Searching for "stacks" in the source code, you'll find quite a few references. Not sure if there's overlap with what you were looking at

[Shujian Yan]

That's great!

[Nick Decroos]

There is also this (deprecated) project: https://github.com/kbuzzard/lean-stacks-project

[Shujian Yan]

Is it possible to have an AI for such thing ^^

[Ruben Van de Velde]

If you can tell us what you mean by that, we can try to answer :)

[Shujian Yan]

An wonderful AI that automaticly translate contents in the Stacks Project to lean code ^^

[Robert Maxton]

"Possible" is a very strong word. But from looking at it, it seems like largely a traditional math textbook, if already formatted nicely and with accessible LaTeX source code, so at least you don't have to do OCR

[Robert Maxton]

That said, the proofs are going to be a real pain. The statements of theorems and definitions are probably easier to do automatically, but the proofs are going to involve filling in a lot of steps most authors consider "trivial" or "obvious"

[Shujian Yan]

For a trivial thing, we may let AI prove it or simply leave it with a "sorry" and then manually solve it later. Since the compiler can check for errors in the translated code, we can leverage the diagnostic to guide AI in correcting the code iteratively. ^^

[Jason Rute]

A few people have mentioned Stacks as the next big challenge in auto-formalization, where the idea is that AI systems would start to formalize stacks and get better as it gets feedback, both human feedback and automatic feedback via RL from trying to prove theorems and make definitions type check, etc. It is certainly a stretch goal, but not an unrealistic one for a group with a lot of motivation (and people and resources).

[Ruben Van de Velde]

I think the more likely path towards formalized stacks results is writing the lean yourself

[Jason Rute]

Probably. But what is the most likely path to building good auto-formalization? :smile: It depends on what your goal is.

[Jason Rute]

Also, it isn’t unrealistic to think that an AI could at least do some simple grunt work at this point. I don’t think we have really stress tested what we can do with LLM based auto-formalization.