The field of formal reasoning is experiencing a significant shift towards the integration of neuro-symbolic approaches, which combine the strengths of neural networks and symbolic methods to achieve improved results. This trend is driven by the potential of neuro-symbolic methods to generate high-quality axiomatic oracles, conjecture useful lemmas, and enhance automated theorem proving. The use of large language models and symbolic techniques is enabling the development of more effective tools for formal reasoning, such as those that can generate proof terms and synthesize programs. Notable papers in this area include:

• Tratto, which presents a neuro-symbolic approach to deriving axiomatic test oracles with high accuracy and precision.
• Lemmanaid, which combines large language models and symbolic methods to conjecture useful lemmas.
• Leanabell-Prover, which demonstrates the potential of posttraining scaling in formal reasoning.
• Canonical, which presents a solver for type inhabitation in dependent type theory.