Part III Mathematics student at the University of Cambridge

Mantas Bakšys

Hi! I am currently a Part III Mathematics student at the University of Cambridge. My research interests lie the broad area of formal mathematics, in which I have already completed sever research internships during my time as an undergraduate. In particular, I am interested in automated proof-discovery using both ML and classical approaches and formalisation of mathematics. Feel free to reach out if you find my research interesting!

Interests
  • Formal theorem proving
  • Automated proof discovery using ML tools
  • Interactive theorem provers and their ecosystems
Education

  • BA & MMath in Mathematics, 2020-2024

    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

 
 
 
 
 
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 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