m∀thl∃ss.lean

Tracks

1. Adversarial Robustness

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).

2. Aeneas

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?

3. Lean as a Haskell Successor

When will we know that production code in Lean makes sense? Would the necessarily liberal use of unsafe and partial undermine all the benefits?

4. Evals and RL Environments

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.

5. CSLib

How related is formalizing the undergrad CS curriculum to providing infrastructure for real world high assurance software?

Operations & Funding

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!

Submissions

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.

Coming Q3 or Q4 2026 to a discord server near you

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