We know a sufficiently powerful reward hacking AI can trick Lean, because humans have tricked Lean (found proofs of False). We'd love to look at results searching for proofs of false, hardening Lean against proofs of false, as well as governance discussions like "should there be a GitHub issue tag for proofs of false?" (as there is in Agda).
Lots of code in the real world is written in Rust. Is the tool for proving Rust code correct in Lean ready for prime time?
When will we know that production code in Lean makes sense? Would the necessarily liberal use of unsafe and partial undermine all the benefits?
We would like to measure how adept language models are at writing code and proving it correct in Lean. If you think of typechecking as a high quality grader, then formal verification challenges also give you a sparse reward signal for negligible cost.
How related is formalizing the undergrad CS curriculum to providing infrastructure for real world high assurance software?
Light touch, no sponsors, pay-what-you-can crowdfunding. Charging a fee helps make sure you actually schedule time in your calendar for a virtual conference—without a nominal fee it's too easy to forget or blow it off.
I'm happy to make an estimate of what my effective hourly rate was as a conference organizer, when all is said and done; with the fee I'm also trying to offset my time / opportunity cost spent organizing this instead of shipping more Lean4 evals.
We will operate in a Discord server spun up just for the event, for its voice & video chat rooms and video streaming features. It'd be cool to do it just in the Lean zulip but I'm telling you the voice and vid chatrooms will add a lot!
You have to apply (gform pending) and a panel of curators have to accept your paper/repo or breakout discussion. Curator profiles will be listed here, with a separate form to apply to be a curator.
email quinn at for-all.dev if you want to help or hinder this project in any way, or to say hi.
m∀thl∃ss.lean