Assumed audience: MSc or PhD Students with interest in Evolutionary Algorithms in Program Synthesis or Theorem Proving.
If you are curious about using Evolutionary Algorithms (Genetic Programming in particular) to Theorem Proving or Program synthesis, consider applying. It consists of funding for spending 3 months in Lisbon working with me.
Automatic Generation of Mathematical Proofs
Mathematicians like Fields Medalist Terrence Tao are now using programming languages like Lean to proof interesting theorems in both known and research-level mathematical areas. The key feature of these languages is Dependent Types, which allow to describe much more interesting properties than regular types like Ints and Floats. You can learn more about this approach here.
The Curry-Howard correspondence shows that programs are proofs, and proofs are programs. The goal of this project is to explore how can Genetic Programming be used to synthesize mathematical proofs. One concern is that the probability of success of a crossover is reduced as common subtrees are less frequent than in symbolic regression or strongly-typed programs.
For evaluation, we plan to use the Lean programming language, and the proof database mathlib, and the LeanGym environment. We also plan to compare with approaches that use Language Models to predict the next step in a proof.
If you have any questions, feel free to reach out to me at me@alcidesfonseca.com