The project aims to design and implement a hybrid automated theorem proving system that tightly integrates deep neural networks for learning proof representations, reinforcement learning for creative proof search, and a symbolic probabilistic module for hypothesizing intermediate lemmas and bridging reasoning gaps.
Lean 4 provides the formal foundation of the system and ensures that all proofs are validated by its kernel. At the same time, Probabilistic Logic Networks maintain formal soundness while allowing the system to benefit from data-driven exploration and learning.