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 the broad areas of Automated Theorem Proving and Formal Mathematics. In particular, I am interesting in application of Machine Learning for proof-discovery in the setting of interactive theorem provers. Feel free to reach out if you find my research interesting!

Interests
  • Automated theorem proving using Reinforcement Learning
  • Formal theorem proving
  • Interactive theorem provers and their ecosystems
Education

  • BA, Mathematics, 2020-2023

    University of Cambridge

  • MMath, Mathematics, 2023-2024

  • PhD, Computer Science, 2024-2028 (expected)

    Computer Lab, University of Cambridge

Publications

Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds (2023). A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs.

Cite DOI URL

Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, Ilya Sutskever (2022). Formal Mathematics Statement Curriculum Learning. Top 25% paper at ICLR 2023.

Cite URL

Mantas Baksys, Xuanang Chen (2021). On number of different sized induced subgraphs of Bipartite-Ramsey graphs (arXiv pre-print).

Cite arXiv

Research Experience

 
 
 
 
 
Contributor
Project Numina
September 2024 – Present Remote
Building autoformalization and prover models in Lean
 
 
 
 
 
Student Researcher
Department of Mathematics and Mathematical Statistics, University of Cambridge
July 2023 – October 2023 Cambridge, UK
  • 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
 
 
 
 
 
Student Researcher
Computer Lab, University of Cambridge
June 2022 – August 2022 Cambridge, UK
  • 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
 
 
 
 
 
Research Intern
Open AI
December 2021 – January 2022 Remote
  • 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
 
 
 
 
 
Student Researcher
Department of Mathematics and Mathematical Statistics, University of Cambridge
June 2021 – August 2021 Cambridge, UK
  • 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