Blockly for Lean

Stream: general

[Alena Gusakov]

Has anyone looked into using Blockly for Lean? I tried searching for it here but couldn't find anything. It's for building visual program editors, similar to Scratch: https://developers.google.com/blockly

[Mario Carneiro]

nope

[Jason Rute]

Why? It looks like the type of programming you do with really little children. I'm not sure lean is at the right level for that?

[Mario Carneiro]

It's also a programming interface, and most of the interesting parts of lean are not about programming

[Jalex Stark]

I think this may be good for getting people that are very-not-technically inclined to get their feet wet, but most of the development energy here is in trying to get research mathematicians to become power users

[Jalex Stark]

If you're interested in combing picture-based software with Lean, I think it would be cool to have graphical proof assistants like globular.science compile into lean code

[Charlie Conneen]

I think a graphical proof assistant would be an outstanding idea. I don't know that blockly is the right tool for getting started with that, though.

[Alena Gusakov]

I was thinking of it as an intro thing, like maybe at the high school level

[Charlie Conneen]

I've heard from friends who don't know Lean that it seems like a "write-only language," which I find amusing. Perhaps if developed, it could be used for high school geometry? They tend to like to tell high schoolers to do those two-column proofs using properties of Euclidean geometry

[Jason Rute]

I mean a lot of math-inclined high school students learn to program in really code (Python, Java, C, BASIC) in high school.

[Jason Rute]

I think something like the NNG is a better use of effort in attracting high school level students.

[Charlie Conneen]

Sure, but I wouldn't compare Lean to those languages. It's not as easy to pick up as some of the languages you listed, but it theoretically could be with a graphical interface. I'm just skeptical as to whether Blockly would be good for that purpose

[Alena Gusakov]

I had the unfortunate experience of going to a high school that used Scratch in their intro to CS course

[Charlie Conneen]

Oh no...

[Alena Gusakov]

So I'm approaching this from that perspective

[Charlie Conneen]

I feel like Lean isn't the best thing to hand high-schoolers interested in CS, if that's where you're going with this

[Alena Gusakov]

I feel like people that are more familiar with math and/or CS at that age are, in my experience, lucky to be introduced to it in a friendly way early on in life

[Alena Gusakov]

No sorry, I was approaching it from the perspective of teaching math

[Charlie Conneen]

I absolutely agree. My high school had no CS courses, and I definitely had to go out of my way to get an enriching education in way of math and CS

[Alena Gusakov]

I'm not in education at all so I may just not know what I'm talking about at all though

[Charlie Conneen]

I definitely romanticize the idea that we could one day have a beautiful graphical interface for Lean, where math proofs would be visual and intuitive for someone at the high school level, but we're admittedly a long ways away from something like that

[Alena Gusakov]

Yeah high school was rough, I have a whole sob story about how bad my high school math education was

[Alena Gusakov]

That's fair, I guess it's something to look into later, for me at least

[Jason Rute]

I think if you want to teach proofs graphically, you could make a graphical block gluing tool with a pretty interface. You could use Lean as a backend or really write your own back end. I don't think there is something special about Lean here. @Michael Beeson a long time ago wrote a GUI Calculus theorem prover for students which didn't let them make mistakes. http://www.helpwithmath.com

[Charlie Conneen]

Well that's impressive. How does the system for creating problems work?

[Scott Morrison]

We could have http://incredible.pm/, with edges carrying local hypotheses, and blocks for have and apply.

[Scott Morrison]

As soon as you plug in a block, under the hood we'd use refine to generate the labels on the input strings.

[Scott Morrison]

unify would determine whether you can join two strings.

[Scott Morrison]

A globular/lean interface would be amazing. You'd get a math-aware programming language to write tactics for globular, and a graphical editor for (higher dimensional) commutative diagrams / rewrite proofs.

[Scott Morrison]

I talked to Jamie Vicary about this a while ago.

[Scott Morrison]

It would be a lot of work.

[Scott Morrison]

There is a zigzag branch that begins formalising their essential data structures.

[Alex J. Best]

Yeah, I really think a lot of the "boring logic lemmas" in lean would have a really wide appeal if there was no notation at all, just puzzles fitting jigsaw pieces together to complete a circuit. incredible seems quite close

[Charlie Conneen]

Yeah! I could totally see a high school propositional logic class being taught using a tool like this

[Jason Rute]

That also reminds me, @Jeremy Avigad once used some graphical propositional logic tool to teach an intro to proofs class.

[Alex J. Best]

I wonder if @Edward Ayers widgets could be leveraged to make a basic version of one of these games in vscode. There was also that cabbage goat wolf thread a long time ago, let me find it.
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/wolf.20goat.20cabbage

[Jason Rute]

I think if you are implementing basic stuff in Lean, you could do that with the lean server which wouldn't be hard. The hard part would be the graphical stuff. (See this thread from today for how to interact with Lean programmatically.)

[Kevin Buzzard]

Jason Rute said:

I think something like the NNG is a better use of effort in attracting high school level students.

I have given many high school talks about the natural numbers and Lean, but induction is not something taught until very late on, so I give the proof of 2+2=4 instead. In fact I had a massive gig in March where I was going to prove 2+2=4 to 250 high schoolers but it got cancelled because of lockdown :-( . I just have it in my head that only the brightest schoolkids would understand induction. I think Euclidean geometry might be a nicer way to introduce Lean to schoolkids, but I have never really thought about it because it would require some graphical UI to be good, and I strongly suspect that there are other systems which can already do this.

[Edward Ayers]

@Alex J. Best this is absolutely a use case of widgets. you could write the whole thing in lean without changing any C++. There are still some features for widgets that are missing like drag and drop though but this was the kind of thing I had in mind.

[Edward Ayers]

The main problem is saving state. At the moment widgets let you 'save state' by returning a string which is put in to the proof document.
But doing this with some graphical structure would look bloaty.

[Jeremy Avigad]

@Jason Rute I think you have in mind Tarski's World (https://www.gradegrinder.net/Products/tw-index.html), which is a great tool for teaching students how to read and write expressions in first-order logic. The exercises are fun. For example, you can give students a list of sentences describing a blocks world ("there is a large tetrahedron to the left of a small cube"), and they have build the world graphically and click a button to see if they got it right. They also have software called Turing's World, which lets students build and run Turing machines.

But these are not about teaching proof. They also have a system for that: https://www.gradegrinder.net/Products/lpl-index.html. I have never used it, but I would be interested in hearing if anyone has had experience with it. It is probably subject to Kevin's objections to e.g. TPIL and Logic and Proof that there is too much emphasis on the logical manipulations, which good mathematics students tend to pick up intuitively, rather than the mathematical content. He has a point: we don't want to convey the impression that proof is only about messing around with ands and ors, it is about drawing substantive conclusions about what follows from what.

Teaching proof with software is hard: a proof is an argument, so you want a fun way for students to construct arguments and get feedback. NNG and friends are probably close to optimal for that. Or something like the Naproche examples, where you pick a restricted domain with a manageable number of definitions and assumptions, write proofs as sequences of statements, and have a first-order theorem prover fill in the rest.

A number of years ago, John Mumma, Ed Dean, and I specified a formal system that allows you to write proofs in elementary geometry much the way you find them in Euclid's Elements. (http://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf) I think it should be possible to implement it, so that students could write proofs in geometry ("Let D be the point bisecting AB. Then AD ~ DB. ..") and have them checked automatically, which a little green check whenever a line is sufficiently justified. In a recent paper, Michael Beeson and co-authors gave us flak for the fact that it hasn't been implemented (they were formalizing geometry in Coq), but I still have hopes of doing it in Lean 4 one day, with nice syntax for writing geometric proofs and interpreting them (in the background) as statements about the Euclidean plane.

[Oliver Nash]

I know nothing about this but for the sake of connecting threads I'll point out that someone has just connected Blockly and Lean: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Blockly.20with.20Lean/near/250457875