How can we call Lean4 from python, exists a lib?

Stream: general

[Daniel Donnelly]

Question in title. Just wondering if anyone has a snippet to share (in Python3 / PyQt5). I want to make something like a Duo Lingo but for learning math. The users will speak in English and there will be a database (Python dictionary or Levenshtein DFA for now) that matches user input to a line of code in Lean4. Because each game is small, "draw the naturality square [for the givens of the Yoneda lemma]". But I want everything to be logically checked using Lean4. I know this sounds ambitious, but I already have the diagram editing part done. I even have different math styles for the arrows working. I might have say all the parts of the diagram in a box on the right. The user then drags/drops/positions the items until the diagram matches. So that wouldn't even require the English-to-Lean4 matching - that particular game. So each game is small, which means the matching task is not out-of-reach as a coder.

[Eric Wieser]

By "a line of code" do you mean something closer to a function call, or to a line in a tactic block?

[Daniel Donnelly]

Eric Wieser, I don't know yet. Good question!

[Daniel Donnelly]

Also, would anyone be down to work on this with me? We could host the code publically on github.

[Eric Wieser]

You might be interested in https://incredible.pm/ (doesn't seem to be usable on mobile, but it's great on the desktop)

[Daniel Donnelly]

The goal is learning software. Because that's I believe where the bottleneck of the world's math understanding is. What good is it if Lean4 "knows" all this math, but we don't know 1/10th of it? That's why gamification of learning is so cool and I'd like to work in that area.

[Daniel Donnelly]

@Eric Wieser that's neat and in the same idea area, however any user input that is foreign to most mathematicians, i.e. any notation / tools that are not English-math + diagrams as seen in a textbook, are off limits to me. I want the software to have close to zero getting started time.

[Daniel Donnelly]

So how the math is presented in the software, that's exactly the format you can communicate back with, with some leeway for typos, other ways of LaTeXing and so on..
With Lean4, we could even do other ways of proof.

[Eric Wieser]

Can you share a screenshot / drawing of what sort of presentation (and an example of the kind of statements you're interested in) you're thinking of?

[Daniel Donnelly]

Anything that can be proven by Lean4 I'm interested in. I'm not converting all English-math into Lean4 nor generating it from code. I'm only needing to match a few examples that the users provide (like Duo Lingo). For example there would be a lot of code re-use because how often do we use statements such as "Let x be in X". And so on... the matcher will know what to write into the formal proof, but these proofs are < 50 lines (usually - think textbook proofs). If the proof checks out, then the user passes go, so each game could actually be Lean4 checked.

[Daniel Donnelly]

What I'm saying is the Levenshtein matcher will only let in a "Levenshtein-fuzzy regular language" around 50 or so possibilities from an alphabet of Lean4 instructions (lines), so in a sense I've broken down the problem of having to convert all of known English-math into Lean4. We just work on a exercise-by-exercise bases, so that that highly complex problem is now easier.

[Daniel Donnelly]

I guess in that case, I could do this without Lean4 though. :)