25 citations · 28 across the 3 of their papers we have counts for
4 papers
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,…
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…