typing up solutions in Lean

Stream: new members

[jessup]

Hello, Lean Prover community.

I have been typing up exercises from the end of chapter one of Atiyah and MacDonald's "Introduction to Commutative Algebra" in LaTeX (via emacs plus auctex). As a commutative algebra student, I wonder if it would be fun to type these up with Lean.

Typing up proofs is reminding me that using LaTeX is already a quasi-programming experience: I tend to try to solve problems on paper, and then go type them up, but the process is never a transcription--I am editing and revising in the language of LaTeX as I type up the hand-written proof.

If I invested the time in energy in getting somewhat conversant in Lean, I wonder if I could use it to type up my solutions to exercises at the end of Chapter 1 in Atiyah-MacDonald? I have no idea. Do you think the technology is there, or not? Maybe it would be accurate to say that I'm interested in Lean from a workflow perspective.

[Scott Morrison]

I think the majority of the material you need for the chapter 1 exercises is in Lean already, so it should be quite doable, but I'm not an expert on the coverage we have on ideals, etc.

[Scott Morrison]

It's an interesting question what to do with such solutions, if you were to produce them.

[Scott Morrison]

Most of the exercises are actually things are are in, or ought to be in, mathlib itself.

[Scott Morrison]

So a second stage might be to find the appropriate names of lemmas, and locations in files, and then integrate the solutions into the library itself.

[Scott Morrison]

It would also, of course, be nice to have them as a document that actually shows the exercise numbers from AM.

[jessup]

(deleted)

[Kevin Buzzard]

@Kenny Lau basically learnt Lean by working through the early chapters of A-M, and this was before we had modules :-) Some of those exercises are hard. We have Spec of a ring as a topological space, but I can't remember whether this is in mathlib or not.

As for writing them up, you could make them look like this https://www.math.u-psud.fr/~pmassot/lean/ :-)

Man, I had better understand what Patrick did and set up my own version of that stuff before Patrick deletes it all.

[jessup]

Wow that link is awesome. Definitely the kind of end-result I had in mind. I am interested in how a technology like Lean can streamline communication about mathematics. With respect to that link, has there been anything interesting on the problem of moving in the other direction (i.e. placing the natural language in the drop-down box). At some level this should be possible, right? Maybe not feasible? Maybe what I'm looking for is a good read by somebody who has already thought a lot about computer-assisted proofs.

[Patrick Massot]

Do you mean generating the natural language from the Lean code? Or do you simply mean displaying stuff differently? Currently everything is typed by a human except for the tactic state, see the source file at https://www.math.u-psud.fr/~pmassot/lean/source.html

[jessup]

I figured the page had been hand coded, but the design did make me wonder about translations between a language like lean and the subset of some given natural language that is used to state proofs in some body of math literature. What about the translation from this source file to the lean test website--is that being done automatically? (btw: studying that page will definitely help me learn to think in terms of lean. Thanks for making it, however you did it.)

[Patrick Massot]

I think there have been experiments to translate from a proof assistant to natural language, but not with Lean. Of course the web page is generated automatically! Doing that by hand would be way beyond my patience. It's produced with https://github.com/leanprover-community/format_lean This is a prototype, this web page is the very first test of that script

[jessup]

haha yes I thought it must be automatic. Thank you for the link