Mechanistic Interpretability and Lean 4

Proposal: implement https://www.arena.education/ in Lean. Why? My intuition is that theorem provers will end up in the final solution to AI safety, if there is one. And if one was devised in “not a theorem prover”, we’d soon want to put it in a theorem prover because the stakes are so high. For all its flaws, mechinterp is the main way I know of to “debug” neural nets. The low level. I’ve already argued for theorem proving and Lean 4 specifically as an endpoint of programming languages. The recent work on agents and programmability seems to support that. I don’t think it’s feasible to fully verify a network (based on Lawrence, Rajashree, and Jason Gross’s work). Even so, it is the time to put deep learning into a theorem prover. Davidad has his ideas for a big cool world alignment theorem prover that I’ve never seen. And if going with Lean is a mistake, it’s an iceberg I want to break upon. Beats waiting. Hopefully, I’ll use the AI to port Lean to your better thing. There are serious…