The field of formal theorem proving and mathematical verification is experiencing significant advancements, driven by innovations in artificial intelligence, machine learning, and semantic search. Researchers are developing novel frameworks and techniques to improve the efficiency, accuracy, and usability of formal proof systems, such as Lean and mathlib. Notably, the development of joint embedding models and retrieval-augmented fine-tuning is enhancing the auto-formalization of natural language proofs, while language models are being trained to simplify proofs without human supervision. Furthermore, semantic search engines are being designed to understand user intents and provide more relevant results. These advancements have the potential to increase the adoption of formal verification methods in various fields, including mathematics, computer science, and industry.

Some noteworthy papers in this area include: ProofBridge, which presents a unified framework for automatically translating entire NL theorems and proofs into Lean 4, achieving substantial improvements in proof auto-formalization. ProofOptimizer, which introduces a language model trained to simplify Lean proofs without requiring additional human supervision, substantially compressing proofs generated by state-of-the-art RL-trained provers. Lean Finder, which proposes a user-centered semantic search tailored to the needs of mathematicians, achieving over 30% relative improvement compared to previous search engines.