The field of proof assistants is undergoing significant developments, particularly in the areas of education and automation. There is a growing trend towards utilizing proof assistants as a tool for teaching and learning, with a focus on creating user-friendly interfaces and interactive tutorials. This shift has the potential to make formal mathematics and computer science more accessible to a wider audience.

In terms of automation, proof assistants are being integrated with automated theorem provers to enhance proof automation capabilities. This integration is crucial for large-scale formal mathematics and software/hardware verification projects. The development of novel translation algorithms and interfaces between proof assistants and automated theorem provers is driving this advancement.

Noteworthy papers include:

• A Graphical Interface for Category Theory Proofs in Coq, which presents a Coq plugin for graphical interface and interaction with categorical proofs.
• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers, which proposes a novel translation algorithm for proof automation in Lean 4.