Showing 1–6 of 6 results for author: Bordg, A

Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

Authors: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, Haitham Bou Ammar

Abstract: Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-gener… ▽ More Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale. △ Less

Submitted 3 July, 2025; originally announced July 2025.

Elements of Differential Geometry in Lean: A Report for Mathematicians

Authors: Anthony Bordg, Nicolò Cavalleri

Abstract: We report on our experience formalizing differential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this effect, we stress the possibly surprising difference between the formalization and its pe… ▽ More We report on our experience formalizing differential geometry with mathlib, the Lean mathematical library. Our account is geared towards geometers with no knowledge of type theory, but eager to learn more about the formalization of mathematics and maybe curious enough to give Lean a try in the future. To this effect, we stress the possibly surprising difference between the formalization and its pen-and-paper counterpart arising from Lean's treatment of equality. Our three case studies are Lie groups, vector bundles and the Lie algebra of a Lie group. △ Less

Submitted 1 August, 2021; originally announced August 2021.

Comments: To appear in the proceedings of the Fifth Workshop on Formal Mathematics for Mathematicians (part of CICM 2021)

MSC Class: 03B35; 53-04

Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types

Authors: Anthony Bordg, Lawrence Paulson, Wenda Li

Abstract: Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the… ▽ More Church's simple type theory is often deemed too simple for elaborate mathematical constructions. In particular, doubts were raised whether schemes could be formalized in this setting and a challenge was issued. Schemes are sophisticated mathematical objects in algebraic geometry introduced by Alexander Grothendieck in 1960. In this article we report on a successful formalization of schemes in the simple type theory of the proof assistant Isabelle/HOL, and we discuss the design choices which make this work possible. We show in the particular case of schemes how the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales. △ Less

Submitted 30 March, 2022; v1 submitted 19 April, 2021; originally announced April 2021.

Comments: Final version accepted for publication in the journal Experimental Mathematics. Our code can be found in the Archive of Formal Proofs, see https://www.isa-afp.org/entries/Grothendieck_Schemes.html

MSC Class: 14A15; 14-04; 03B16; 03B35; 68V20 ACM Class: G.m

Journal ref: Experimental Mathematics, 31:2 (2022), 364-382

Certified Quantum Computation in Isabelle/HOL

Authors: Anthony Bordg, Hanna Lachnitt, Yijun He

Abstract: In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix… ▽ More In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory. △ Less

Submitted 27 December, 2020; originally announced December 2020.

Comments: J Autom Reasoning (2020)

MSC Class: 03B35; 03B15; 81P68; 68Q12

Comment on "Quantum Games and Quantum Strategies"

Authors: Anthony Bordg, Yijun He

Abstract: We point out a flaw in the unfair case of the quantum Prisoner's Dilemma as introduced in the pioneering Letter "Quantum Games and Quantum Strategies" of Eisert, Wilkens and Lewenstein. It is not true that the so-called miracle move therein always gives quantum Alice a large reward against classical Bob and outperforms tit-for-tat in an iterated game. Indeed, we introduce a new classical strategy… ▽ More We point out a flaw in the unfair case of the quantum Prisoner's Dilemma as introduced in the pioneering Letter "Quantum Games and Quantum Strategies" of Eisert, Wilkens and Lewenstein. It is not true that the so-called miracle move therein always gives quantum Alice a large reward against classical Bob and outperforms tit-for-tat in an iterated game. Indeed, we introduce a new classical strategy that becomes Bob's dominant strategy, should Alice play the miracle move. Finally, we briefly survey the subsequent literature and turn to the 3-parameter strategic space instead of the 2-parameter one of Eisert et al. △ Less

Submitted 21 November, 2019; originally announced November 2019.

MSC Class: 81P40 81P45 91A05 91A10 91B80

Univalent Foundations and the UniMath Library

Authors: Anthony Bordg

Abstract: We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas, followed by a discussion of the UniMath library of formalized mathematics implementing the ideas of the Univalent Foundations (section 1), and the challenges one faces in attempting to design a large-scale library of formalized mathematics (section 2). This leads us to a general discussion about th… ▽ More We give a concise presentation of the Univalent Foundations of mathematics outlining the main ideas, followed by a discussion of the UniMath library of formalized mathematics implementing the ideas of the Univalent Foundations (section 1), and the challenges one faces in attempting to design a large-scale library of formalized mathematics (section 2). This leads us to a general discussion about the links between architecture and mathematics where a meeting of minds is revealed between architects and mathematicians (section 3). On the way our odyssey from the foundations to the "horizon" of mathematics will lead us to meet the mathematicians David Hilbert and Nicolas Bourbaki as well as the architect Christopher Alexander. △ Less

Submitted 17 November, 2019; v1 submitted 7 October, 2017; originally announced October 2017.

MSC Class: 03B15 03B35

Journal ref: In: Centrone S., Kant D., Sarikaya D. (eds) Reflections on the Foundations of Mathematics. Synthese Library, vol 407, 2019. Springer, Cham