Reverse direction - from Lean proof to human proof

Stream: new members

[Ilmārs Cīrulis]

Let's suppose that I've made a formal proof (as good as possible for me) and now I want to present it to some hypothetical humans in the form of "human" proof.

Are there any suggestions how to do that? Or is it mostly something like "be fluent at presenting math in the first place"? :sweat_smile:

[Ilmārs Cīrulis]

For now I will take a look at Lean Verso and try to learn to use it.

[Snir Broshi]

This reverse direction is called "informalizing", the reverse of formalizing
There are a few tools (I'll send some shortly), but there's still a lot of room for innovation in this space

[Snir Broshi]

• See the links in #Is there code for X? > Lean Informal
• David Renshaw's tool https://www.youtube.com/watch?v=KuxFWwwlEtc
  and examples of using it:
  https://www.youtube.com/watch?v=gi8ZTjRO-xI
  https://www.youtube.com/watch?v=5IARsdn78xE
  
  
  

[Ilmārs Cīrulis]

(deleted)

[Ilmārs Cīrulis]

(deleted)

[Snir Broshi]

Please open a topic for that, it's not related to the current topic

[Ilmārs Cīrulis]

Verbose Lean is an useful tool for this too, I believe, even if its approach is a bit different.

[suhr]

Are there any suggestions how to do that?

Start with restructuring and adding type annotations to make your formal proof readable. Then translate it into prose. Then rewrite your prose a few times to make it actually readable.

[suhr]

Observe that a formal proof can be unreadable mess, but it also can be clean and clear. So readability is not a result of translating from Lean to native language, it's a result of organized presentation that communicates ideas and focuses on what is relevant.

[James E Hanson]

Snir Broshi said:

This reverse direction is called "informalizing",

I know this is semi-standard terminology at this point, but I find the convention of referring to ordinary mathematics as 'informal' maybe a little bit offensive to be completely honest.

[Snir Broshi]

James E Hanson said:

I know this is semi-standard terminology at this point, but I find the convention of referring to ordinary mathematics as 'informal' maybe a little bit offensive to be completely honest.

Well, informal ≠ non-rigorous, formality refers to doing math/logic by pure symbol manipulation in a formal system (such as a Hilbert system). e.g.

• https://en.wikipedia.org/wiki/Modus_tollens#Formal_proof
• https://en.wikipedia.org/wiki/Deduction_theorem#Examples_of_deduction
• https://en.wikipedia.org/wiki/Hilbert_system#Proof_example_in_P2

and since when doing ordinary mathematics no one writes such tedious tables of justification, they are rigorous but informal.

[Snir Broshi]

I like the explanation in 5:26 - 5:41 at https://www.youtube.com/watch?v=MJrYwh6WyF8&t=5m26s
image.png

[suhr]

I should point out that Hilbert system is a rather poor example of a formal system: very awkward to use and with no good structural properties.

[James E Hanson]

Snir Broshi said:

Well, informal ≠ non-rigorous, formality refers to doing math/logic by pure symbol manipulation in a formal system (such as a Hilbert system). e.g.

I understand that 'formal' is being used in a technical sense here, but it's also something that mathematicians use in other senses. People talk about 'formalizing' an intuition in the sense of finding a more specific notion that captures it. They'll also say that certain proofs are 'purely formal', meaning they just involve symbol pushing.

In any case, you can justify it however you want. I'm just reporting the fact that a lot of mathematicians would be annoyed by the implication that every proof they've ever written is 'informal'. The word 'informal' has a pretty specific connotation in math of 'not doing it for real'.

[Ruben Van de Velde]

Thanks for sharing - though I don't know whether it'll change the established meaning in the formalizing community

[James E Hanson]

Sure, I wouldn't think it would. There's plenty of examples of different parts of math disagreeing about what words mean, and these typically don't get resolved.

[Ilmārs Cīrulis]

This borders on off-topic, but still...

I decided to start my attempts to write the math prose, uff, and I should learn some more English... :sweat_smile: From math books, probably.
Is there some place (on the Internet in general) where to put or link to such attempts and get some reviews/criticism/suggestions?

Thank you!