research
∙
08/01/2021
Elements of Differential Geometry in Lean: A Report for Mathematicians
We report on our experience formalizing differential geometry with mathl...
share
research
∙
04/19/2021
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types
We report on a formalization of schemes in the proof assistant Isabelle/...
research
∙
12/27/2020
Certified Quantum Computation in Isabelle/HOL
In this article we present an ongoing effort to formalise quantum algori...
research
∙
11/21/2019
Comment on "Quantum Games and Quantum Strategies"
We point out a flaw in the unfair case of the quantum Prisoner's Dilemma...
research
∙
10/07/2017