Generating manga from a formal proof

Stream: new members

[Yasuaki Morita]

I am now interested in generating manga from formal proofs because it makes it easier for me to read. I think there is a tool that generates a natural language from a proof in lean (heard from Dagur Ásgeirsson). I did a little searching but couldn't find it.
Please let me know of any similar tools or related ideas.

[Kyle Miller]

The source code's not available yet, but here are a couple examples: https://kmill.github.io/informalization/rudin.html and https://kmill.github.io/informalization/ContinuousFrom.html (starting from https://kmill.github.io/informalization/rudin.lean.txt and https://kmill.github.io/informalization/ContinuousFrom.lean.txt)

[David Renshaw]

Kyle Miller said:

The source code's not available yet

When will it be?

[Luigi Massacci]

@Patrick Massot is Jacques Tardi going to be the next postdoc in Orsay...?

[Patrick Massot]

Why specifically Tardi? Do you see weird monsters in your Lean files?

[Kevin Buzzard]

I would be interested in a clarification of the meaning of the word "manga" in the context of the title of this thread.

[Yasuaki Morita]

In this thread, a manga consists of a picture of two or so characters and a line of dialogue about the flow of proof. Here is a concrete example (in Japanese):
https://rookie.shonenjump.com/series/EmTZ65sIcQU
The story is about someone going to Goldbach Gym to understand the proof of Hilbert's tenth problem. Despite there is little narrative depth or pictorial beauty, it still helps me to follow the flow of proofs. Reading formal proofs is quite a painful task (as is proof on paper sometimes). It is quite psychologically pleasing to disguise some kind of dialogue element, like teddy bear pair programming or rubber duck debugging.

[Yasuaki Morita]

Kyle Miller said:

The source code's not available yet, but here are a couple examples: https://kmill.github.io/informalization/rudin.html and https://kmill.github.io/informalization/ContinuousFrom.html (starting from https://kmill.github.io/informalization/rudin.lean.txt and https://kmill.github.io/informalization/ContinuousFrom.lean.txt)

Thank you! I'd like to know a little more about the technical details (even if I can't see the source code itself). Do you use any AI technology like ChatGPT?

[Patrick Massot]

See https://www.youtube.com/watch?v=tp_h3vzkObo

[Mark Fischer]

I think paperproof is headed a really great direction in the way it inspects/displays changes to the proof state. This is closer to interactively stepping through the proof state in an editor.

It might give you some ideas!

[Luigi Massacci]

Echoing what @Treq said, if you want to work on graphical presentations, you could also take a look at Actema, which is a graphical interface for Coq. Here is a very short abstract about it, and you can listen to this talk for something more in depth. I don’t know how much @Pablo Donato uses Zulip.

[Pablo Donato]

Thanks for mentioning Actema @Luigi Massacci! However if I understand correctly, @Yasuaki Morita is looking for a nicer presentation of formal proofs for reading them, whereas Actema is (currently) focused on offering a nicer interaction with goals for writing proofs.

[Yasuaki Morita]

@Treq @Luigi Massacci @Pablo Donato Actually, what was in my mind was not graphical presentations for writing proof. Manga is just a random idea that would drive me psychologically to read long proofs written by someone else (or myself).