Lean Informal

Stream: Is there code for X?

[Alfredo Moreira-Rosa]

Sorry if this was asked a million times already, but i can't find any sources.

Given this video from @Patrick Massot two years ago about lean informal : https://www.youtube.com/watch?v=tp_h3vzkObo

Was there any advancement on this project ? Was the goal changed to Lean Blueprint ?

[Michael Rothgang]

There are now two public demos for the project output, at https://kmill.github.io/informalization/rudin.html and https://kmill.github.io/informalization/ContinuousFrom.html.

My understanding that is that this project made a lot of progress, but some significant work is needed to push it to completion/being usable on e.g. a generic mathlib proof. Basically, it's a matter of Massot and Miller finding enough unobstructed time, i.e. blocked on finding some funding to buy out such time. If you sit on a bag of money for one person-year, this could be a useful contribution!

Was the goal changed to Lean Blueprint?

I'm quite puzzled by this question. Formal-to-informal translation and the blueprint software are two very different things. If you mean something else, please provide enough context so this is understandable without watching the video.

[Michael Rothgang]

(deleted)

[Alfredo Moreira-Rosa]

Michael Rothgang said:

I'm quite puzzled by this question. Formal-to-informal translation and the blueprint software are two very different things. If you mean something else, please provide enough context so this is understandable without watching the video.

Sorry if any confusion, i meant: "Was the goal of creating informal abandonned/changed to instead work on Blueprint because Blueprint has more direct value for the community ?"
And i understand that it's abandonned for lack of time.

[Patrick Massot]

The blueprint software is much older, it was started (and already used) in 2020, although it's true that I worked a lot in early 2024 to make it easier to use. Informal Lean is not abandoned, it is not currently moving but work will resume, hopefully soon.