31 citations · 52 across the 8 of their papers we have counts for
6 papers · 1 filter
A formalization of the Gelfond-Schneider theorem
Michail Karatarakis, Freek Wiedijk
We formalize Hilbert's Seventh Problem and its solution, the Gelfond-Schneider theorem, in the Lean 4 proof assistant. The theorem states that if and are algebraic numbers…
Proof-checking Euclid
Michael Beeson, Julien Narboux, Freek Wiedijk
We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a l…
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
Freek Wiedijk
We propose a synthesis of the two proof styles of interactive theorem proving: the procedural style (where proofs are scripts of commands, like in Coq) and the declarative style (w…
Stateless HOL
Freek Wiedijk
We present a version of the HOL Light system that supports undoing definitions in such a way that this does not compromise the soundness of the logic. In our system the code that k…
Pure Type Systems without Explicit Contexts
Herman Geuvers, Robbert Krebbers, James McKinna +1
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments o…
Proviola: A Tool for Proof Re-animation
Carst Tankink, Herman Geuvers, James McKinna +1
To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof m…