lean for presentation

Stream: general

[Felix Benning]

Is there any attempt at converting lean code into interactive proofs? I mean LaTeX could never do that because it does not actually understand the proof. But if there was a way to "render" lean proofs, you could click on an equal sign or implication and lean could add additional information. Has anybody thought about this yet? I.e. Proof assistants to generate Math presentation?

[Arthur Paulino]

Do you mean slides? Or any interactive means?
Alectryon can create pages with hover handles for Lean 3. And there's a WIP integration of Alectryon and LeanInk for Lean 4

[Henrik Böving]

In Lean itself we have @Patrick Massot work on teaching the tactic system a form of natural languagehere in french: https://github.com/PatrickMassot/lean-bavard and here the English port: https://github.com/PatrickMassot/lean-verbose. The Isabelle/HOL system has made huge efforts over the years to make their proofs as readable as normal mathematical text using an extension upon their basic system that is called Isar, however integrating such a thing into Lean would first require us to develop the insane amount of automatic reasoning Isabelle already has. Regarding theorem prover mathematics it's the closest thing I know to just ordinary mathematical texts.

We also have some work going on on porting the Coq tool https://github.com/cpitclaudel/alectryon to Lean 4 here: https://github.com/leanprover/LeanInk this doesn't exactly make the proof itself more readable, but the static presentation of the proof outside of an editor becomes much more interactive and we could for example render proofs about trees as actual trees in HTML.

[Arthur Paulino]

This thread is reasonably recent on the topic of LeanInk + Alectryon

[Felix Benning]

@Arthur Paulino I mean interactive webpages - something more advanced than this https://mannheim-probability.github.io/Probability-Theory/exercises/sheet_7.html (which is the result of applying latexml to existing latex documents and adding javascript which turns the solutions into collapsible html elements - which is the only interactive element so far).

[Felix Benning]

for example being able to get incrementally more explicit hints or having your solution checked etc

[Henrik Böving]

That would be absolutely amazing but I don't think something like this is even close to what we can reasonably provide at the moment.

[Henrik Böving]

At least not automatically generated, you could have the math texts handwritten and backed by lean code of course.

[Arthur Paulino]

Do you mean having a Lean kernel running in your browser, being able to communicate with a remote Lean kernel or something like that?

[Felix Benning]

anything really - just wanted to know what efforts there were so far in this direction. Will read up on all the links provided now :)

[Arthur Paulino]

Have you seen the Natural number game?

[Felix Benning]

yes I have - amazing! :)

[Felix Benning]

that was my first contact with lean - what I noticed there is that it is kind of like giving directions a la

1. go 30 steps southeast
2. turn 20 degrees to the right and go 20 steps
3....

In contrast to how math is usually laid out

To the south east you should see a watertower, go to that

i.e. provide landmark equations and some sentences in-between but leave the actual steps to the reader.

[Patrick Massot]

Felix, you can have a look at https://www.imo.universite-paris-saclay.fr/~pmassot/files/exposition/why_formalize.pdf to see you're not the only one dreaming here. Clearly we need a way to turn Lean file into interactive document that look like ordinary math texts except you can ask to see more details anywhere you like.

[Patrick Massot]

As usual here, the answer is that we wait for mathlib in Lean 4 before doing serious work.