25 citations · 45 across the 10 of their papers we have counts for
11 papers
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
Anthony Bordg
AlphaGeometry represents a milestone in neuro-symbolic reasoning, yet its architecture faces a log-linear scaling bottleneck within its symbolic deduction engine that limits its ef…
Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov +3
Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rew…
Elements of Differential Geometry in Lean: A Report for Mathematicians
Anthony Bordg, Nicolò Cavalleri
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,…
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
Anthony Bordg, Lawrence Paulson, Wenda Li
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 setti…
Certified Quantum Computation in Isabelle/HOL
Anthony Bordg, Hanna Lachnitt, Yijun He
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…
Comment on "Quantum Games and Quantum Strategies"
Anthony Bordg, Yijun He
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 Lewens…
On a model invariance problem in Homotopy Type Theory
Anthony Bordg
In this article the author endows the functor category [B(Z2),Gpd] with the structure of a type-theoretic fibration category with a univalent universe using the so-called injective…
On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom
Anthony Bordg
In this article the author endows the functor category [B(C2),Gpd] with the structure of a type-theoretic fibration category with a universe using the projective fibrations. It off…
Univalent Foundations and the UniMath Library
Anthony Bordg
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 imple…
The Interpretation Lifting Theorem for C-Systems
Anthony Bordg
In this article we present a solution to a conjecture of Vladimir Voevodsky regarding C-systems. This conjecture provides, under some assumptions, a lift of a functor $M\colon \mat…
On lifting univalence to the equivariant setting
Anthony Bordg
This PhD thesis deals with some new models of intensional type theory and the Univalence Axiom introduced by Vladimir Voevodsky. Our work takes place in the framework of the defini…