lean4-balance-car

Stream: lean4

[Andrew Kent]

We've got an initial version of our Lean4-controlled self-balancing car up and running for anyone interested: https://github.com/galoisinc/lean4-balance-car

This was a small proof-of-concept exercise to show Lean programs controlling a real robotics platform which requires low latency and accurate calculations (less the robot tip over)---it did not involve anything more exotic like modeling the real world physics, proving properties about the controller, etc.

[Bryan Gin-ge Chen]

The video is cool!

[Joe Hendrix]

I should say a bit more about the longer term goals at Galois. In general, I think it'd be really great to see Lean 4 being treated as a practical, if esoteric, programming language.

The idea would be, we just write programs using Lean instead of some other language. If there are particular parts that we want to at some point show correct or reason about, we don't have to rewrite the component in a theorem prover to get started -- it's already in a formal language. We may have to modify it a bit to make the code pure or isolate the most critical parts, but we can keep using the Lean code as the actual implementation.

There might be some overlap with mathlib where perhaps enough of mathematics is formalized that mathematicians feel comfortable with formalizing the bits of the problem or proof they really care about using existing work, and then use Lean's theorem proving capabilities first to show those parts are good.

[Kevin Buzzard]

My impression is that what the Lean developers would like right now is just a whole bunch of random code doing random things written in Lean 4, so they can figure out what works and what doesn't. This is a never-ending quest of course -- look at C++, it's used by a gazillion people and they've been tweaking the language for decades and still continue to tweak it, presumably because of requests from the user base. This is why I decided to try to (slowly) do filters in Lean 4, because the maths is all fresh in my head from teaching it and it would just be a neat way to check that things work out. Of course they worked out very smoothly in Lean 3 so I am not expecting any surprises.

[Joe Hendrix]

I thought I'd mention here. We just put out this blog post describing the robotics experiments we've done so far. It's a bit aspirational at the moment, but I've also created a Real-time Systems Zulip channel here in case people have questions or other efforts involving Lean in real-time systems.