PhD student in Computer Science, University of Cambridge
Mantas Bakšys
I am a PhD student at the Computer Lab, University of Cambridge supervised by Prof. Sean Holden. My research interests lie in the broad areas of Automated Theorem Proving and Formal Mathematics. In particular, I am interested in application of Machine Learning for proof-discovery in the setting of interactive theorem provers. I have experience working with reinforcement learning techniques for formal reasoning, having contributed to state-of-the-art models for autoformalization and proving in Lean. Feel free to reach out if you find my research interesting!
- Automated theorem proving using Reinforcement Learning
- Formal theorem proving and verification
- Interactive theorem provers and their ecosystems
PhD, Computer Science, 2024-2028 (expected)
University of Cambridge
MMath, Part III Mathematics, 2023-2024
University of Cambridge
BA (Hons), Mathematics, 2020-2023
University of Cambridge
Publications
Research Experience
- Supervised by Dr. Stefan Zetsche, working on Reinforcement Learning for program verification
- Developing novel RL approaches for automated theorem proving and formal verification
- Using RL techniques to train AI models for Interactive Theorem Proving in Lean
- Development of Lean-Python interfaces for dataset and benchmark creation and curation
- Released open-source models for autoformalization and proving in Lean with state-of-the-art performance on the miniF2F benchmark
- Worked in a research group led by Professor Timothy Gowers on automated theorem-proving
- Focus on motivated proof discovery using the Lean theorem prover
- Jointly developed an interactive Lean program to guide further research in human-oriented theorem proving
- Worked in the ALEXANDRIA group supervised by Dr Angeliki Koutsoukou-Argyraki
- Successful formalisation of Master’s level material in Additive Combinatorics including the Balog-Szemeredi-Gowers theorem
- Co-authored a paper accepted to CPP 2023
- Worked with Stanislas Polu on training ML models to find formal proofs using the Lean theorem prover
- Analyzed properties of trained models and investigated new research directions
- Co-authored a paper accepted to ICLR 2023
- Worked with Dr Aled Walker on a Summer Research Placement spanning 8 weeks
- Investigated the Multiplication Table problem for bipartite graphs
- Co-authored a paper pre-print
Talks
Joint invited talk with Jonas Bayer presenting Kimina Prover. AITP 2025 Conference, Aussois, France, September 2025.
Presented Kimina Prover to the AWS Reasoning Group. Amazon Web Services (AWS), London, UK, August 2025.