In my view, AI currently relies primarily on human-developed tools for verification. Although AI has used some reinforcement learning (RL) algorithms to identify the paths humans have taken at each level, these paths are essentially still based on human mathematical tools and require confirmation by human experts. We need a more revolutionary framework to provide AI for mathematics with new methods and verification pathways.

Applications: implications, simulations, and experiments. Gobble the frontier; wring out the usable.

make no mistakes

mostly jk, although agents themselves are of course getting better at detecting whether a formal spec is faithful to a natural language spec

You don't. You place unwavering faith in the machine god.

This is why, for formal methods to really be the next step, we'll need deterministic source to CoC language compilers, and we'll need to go back again.

Lean is kind of an unfortunate, cargo cult choice because it only compiles to C. Really for software we should use a prover that has a lot more targets, like Danfy. Even Rocq (formerly Coq) can compile down to several functional languages, which is more than we can say for lean.

As usual, the AI crowd latched on to the first solution that came to mind, and thanks to its prominence in mathematics applications recently just lazily are starting to try and apply it to computing, without actually understanding anything or weighing trade offs. Of course, now we are basically stuck with Lean since the models will have been trained hard on it. At least it's a CoC language, but now we need to build a bunch of extra compilation around it for this to really work.