Zulip Chat Archive

Stream: new members

Topic: typing up solutions in Lean


view this post on Zulip jessup (Feb 08 2019 at 02:40):

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.

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:13):

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.

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:13):

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

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:13):

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

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:14):

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.

view this post on Zulip Scott Morrison (Feb 08 2019 at 04:14):

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

view this post on Zulip jessup (Feb 08 2019 at 04:23):

(deleted)

view this post on Zulip Kevin Buzzard (Feb 08 2019 at 07:24):

@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.

view this post on Zulip jessup (Feb 10 2019 at 21:16):

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.

view this post on Zulip Patrick Massot (Feb 10 2019 at 21:19):

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

view this post on Zulip jessup (Feb 10 2019 at 21:33):

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.)

view this post on Zulip Patrick Massot (Feb 10 2019 at 21:42):

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

view this post on Zulip jessup (Feb 10 2019 at 21:44):

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


Last updated: May 11 2021 at 14:11 UTC