We have proof automation now

The blog post discusses the challenges and possibilities of using dependently-typed languages like Lean for proof automation in software development. It highlights the potential of automating proof efforts with recent advancements like LLMs, compares Lean with other languages, shares personal experiences of proof efforts, and introduces a practical project—building a Zstandard decompressor in Lean. The author reflects on the implications of combining LLMs with dependent types for improving software engineering workflows.