Finding a Lean to English analysis project

Stream: general

[Gareth Ma]

I remember seeing a project (in fact a talk presenting it) that turns Lean code into English, basically by translating line by line. It turns something like

example : Tendsto f atTop (nhds 0) := by rw [Metric.tendsto_nhds_iff_dist_ball_thing] intro eps h_eps let delta := eps / 2 use delta ...

into English

We want to show that $f(x)$ tends to $0$ as $x$ tends to $\infty$
A function $f$ tends to $c$ if and only if $\forall \epsilon > 0$, <delta, ...>
Let $\epsilon$ be an arbitrary positive real number.
Let $\delta = \epsilon / 2$.
Then ...

it's just line by line translation. Does anyone know which project that is?

cc @Julian Berman :D

[Eric Wieser]

https://kmill.github.io/informalization/rudin.html ?

[Gareth Ma]

Looks vyer much like it!!! Thanks :)

[Xiyu Zhai]

Interesting!!! Is there any source code for this? I googled "kmill github informalization" but it doesn't give me anything related.

[Julian Berman]

I think the source for what you see is here -- but the tool to do it isn't there.
I have vague recollection that @Kyle Miller mentioned in some other thread that it may not be public (because it was still a POC?) but I could be wildly misremembering.

[Xiyu Zhai]

Great, thanks a lot!

[Xiyu Zhai]

My brief glance gives me the impression that this is based on symbolic ai. I wonder is there a linguistic component in the project? I personally am interested in bringing back the value of symbolic ai and linguistics in the context of llms. This seems a promising direction. Is there any timeline on published work or info?

[Mario Carneiro]

Yes, the tool which does this informalization is not public, which is quite frustrating to me (as I have already expressed to @Patrick Massot ) because I have projects that would like to build upon this tool and are currently in a holding pattern until it is released

[Xiyu Zhai]

Personally I believe informalization is a direction where many research could be conducted to find the best way to do things. And I believe we should make things as open as possible. A closed source translation loses much of the trust we could have on a symbolic system.

[Eric Wieser]

I think you're confusing "closed source" (a black box exists but you can't see what's inside) with "unreleased" (you don't get the black box)

[Xiyu Zhai]

I see

[Xiyu Zhai]

So probably we will see it open in the near future.

[Kyle Miller]

Thanks for all of your interest everyone —we will make these informalization tools available once they're ready for others to build on them, and it will certainly be open source.

@Xiyu Zhai Your impression is correct, it's symbolic. We want to feel confident that translations are correct (or at least incorrect in systematic ways that we can fix :-) )

I am hoping to see some things finally released in the next month or two.

[Xiyu Zhai]

Exciting. I’m curious how it handles things like compactifying conditions as adjectives and stuffs.

[Xiyu Zhai]

I’m eager to see complementary approaches to LLMs. These days people forgot there are other options for translation besides llm

[Eric Paul]

The examples seem really great! @Kyle Miller is there any update on the progress releasing this?

[Patrick Massot]

There is no update, sorry.

[Kyle Miller]

Patrick and I are thinking about it though and do still plan to release it.