Your guide to formal verification when machines write Lean proofs

Formal verification of software is cheaper than ever. AI agents are writing proofs in theorem provers like Lean. But how do you know what's proved in theorem provers corresponds to reality? Anyone who is interested should be able to compare definitions in theorem provers against what they know. The first good step is to use simpler programming languages that can be described in a few pages rather than languages that take tens of thousands of pages to describe.