The field of automated theorem proving is witnessing significant advancements with the integration of machine learning and formal verification techniques. Researchers are exploring new approaches to improve the efficiency and effectiveness of theorem proving, including the redesign of proof languages and the development of novel formalisms for representing proofs.

One of the key directions in this field is the use of large language models (LLMs) to automate formal proofs. These models have shown promise in reducing the labor costs and computation costs required in proof engineering. Furthermore, the development of tool-integrated reasoning models is enabling the creation of more sophisticated and human-like problem-solving strategies.

Another area of focus is the development of new formalisms for representing proofs, such as scroll nets, which provide a topological notation for implication. These formalisms have the potential to improve the logical and computational expressivity of automated theorem proving systems.

Noteworthy papers in this area include:

• IsaMini: Redesigned Isabelle Proof Language for Machine Learning, which introduces a redesigned proof language for Isabelle/HOL that improves the success rate of neural theorem proving.
• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving, which proposes a lemma-style whole-proof reasoning model that achieves state-of-the-art results on several benchmarks.