WE HAVE PROOF AUTOMATION NOW

Summary from the TLDR AI newsletter

The problem with great type-system power is that it requires great proof effort. Doing proofs can be fun, but they take a lot of time. It can take hours of effort to discover that what you were trying to prove was false. This overhead has made programming in dependently typed languages extremely niche. It has also spurred people to try and automate it away. LLMs promise to be an extremely capable form of proof automation.