Formalising Fermat

Stream: FLT

[Xiyu Zhai]

I wouldn’t bet on formalising FLT using Lean alone. I would bet on inventing more convenient tools (with much better human computer interaction) that complements Lean. I plan on dedicating myself to that purpose in the following years.

[Somo S.]

hey, what if you invented those very tools using lean.. wouldnt that be great!

[Ruben Van de Velde]

Please move further discussion to the #FLT stream

[Notification Bot]

3 messages were moved here from #announce > Formalising Fermat by Johan Commelin.

[Kevin Buzzard]

Obviously I _would_ bet on formalising FLT using Lean alone, because other very large formalisation projects have succeeded and I can see a path to the goal. However I am all for using more convenient tools, and am enthusiastic about such ideas until people start talking about feeding LaTeX of complicated maths papers into a machine and getting Lean out, when I start quietly rolling my eyes about the over-optimism of computer scientists (my personal guess is that we will have finished the formalisation before AI gets to that point).

[Chris Birkbeck]

Well LaTeX to sorry-free Lean (that actually proves the original statement) does sound a bit far I agree, but LaTeX to some sorry-full Lean might be there before FLT is done, at least that's my hope.

[Chris Birkbeck]

But I agree, I think Lean should be able to do FLT fine without anything else.

[Ruben Van de Velde]

That is, of course, assuming you've got a sufficiently detailed latex in the first place

[Chris Birkbeck]

Oh yeah better than anything I've ever written for sure!

[Kevin Buzzard]

Right -- part of the project is writing a clear LaTeX proof.

[Alex Kontorovich]

LaTeX to sorry-full (and error-full) Lean already exists, namely copilot. (The general purpose but huge parameter one trained by Microsoft seems, at least to me, in practice, to currently do better than Lean/specific trained ones like LeanCopilot…) I’ve found it extremely useful to have the natural language blueprint side by side with lean, both of which are often auto-generated and say almost exactly what I want…

[Kevin Buzzard]

So what happens if you just put the LaTeX source code of e.g. Darmon-Diamond-Taylor into copilot?

[Chris Birkbeck]

Alex Kontorovich said:

LaTeX to sorry-full (and error-full) Lean already exists, namely copilot. (The general purpose but huge parameter one trained by Microsoft seems, at least to me, in practice, to currently do better than Lean/specific trained ones like LeanCopilot…) I’ve found it extremely useful to have the natural language blueprint side by side with lean, both of which are often auto-generated and say almost exactly what I want…

Hmm interesting. I've also been using this, but haven't had a latex also open at the same time. I find it hard to know what it looks at to generate the suggestions.

[Alex Kontorovich]

Kevin Buzzard said:

So what happens if you just put the LaTeX source code of e.g. Darmon-Diamond-Taylor into copilot?

Great question! Someone should try it :) (In my experience, for copilot to be effective, needs to do this little lemma by little lemma…)

[Alex Kontorovich]

Chris Birkbeck said:

Hmm interesting. I've also been using this, but haven't had a latex also open at the same time. I find it hard to know what it looks at to generate the suggestions.

It’s not that I have TeX open in some other file (I think copilot only reacts to one file at a time); I have them both open in the same file. See, e.g. here. This is how we’ve been generating the whole blueprint for PNT+…

[Chris Birkbeck]

Oh interesting! I wondered if they were just both open in VSCode, since I remember hearing that copilot looks at the open files or something like that. But this is more like what I would want anyways, you write the latex first and then it guesses the lean.

[Alex Kontorovich]

Exactly. And then we have blueprint scrape out the TeX and make a dependency graph, etc… I find it really fun and productive to work this way…

[Kevin Buzzard]

Oh this hadn't occurred to me! I have a bunch of LaTeX which Taylor wrote on FLT, I should try this :-)

[Alex Kontorovich]

Here’s the script we wrote to execute this: https://github.com/ianjauslin-rutgers/leanblueprint-extract

[Kevin Buzzard]

So lemme get this straight. You're writing the latex blueprint first, dumping it into a lean file in comments, and then using copilot to write the corresponding lean code, and then doing a final edit on the blueprint to add in the name of the lean function which you got copilot to help you generate?

I'm a week or two away from beginning years of doing this, so I'm very interested to hear about your workflow!

[Alex Kontorovich]

No, I write the latex blueprint right in the lean file. Let's hop on a zoom call so I can show you...

[Patrick Massot]

Isn’t it super painful to loose editor support for TeX? I couldn’t type TeX without the vimtex plugin. Or do you have a trick to simultaneously have Lean and TeX support in your editor?

[Kevin Buzzard]

The only TeX support I'm using in my editor (emacs) is ctrl-C ctrl-C to compile, and I could just as easily be pressing up-arrow enter in a terminal.

[Patrick Massot]

Your life could be a lot nicer then.

[Kevin Buzzard]

yeah but if you don't tell me this then I'll be very happy to learn Alex's tricks.

[Alex Kontorovich]

By the way, if you use emacs, then you could get @Paul Nelson's hacks, and see the LaTeX compiled inside the lean!... (I'm very jealous of that feature, which doesn't seem to be available in VSCode. It's almost tempting enough to get me to switch to emacs. Almost...)

[Newell Jensen]

Alex Kontorovich said:

By the way, if you use emacs, then you could get Paul Nelson's hacks, and see the LaTeX compiled inside the lean!... (I'm very jealous of that feature, which doesn't seem to be available in VSCode. It's almost tempting enough to get me to switch to emacs. Almost...)

screenshot? I am curious what that looks like.

[Alex Kontorovich]

Paul had posted one here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/blueprint.20changes/near/411609785