31 citations · 52 across the 8 of their papers we have counts for
8 papers
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…
Formalized Hopfield Networks and Boltzmann Machines
Matteo Cipollina, Michail Karatarakis, Freek Wiedijk
Neural networks are widely used, yet their analysis and verification remain challenging. We present a Lean~4 formalization covering both deterministic and stochastic models. We fir…
A benchmark for C program verification
Marko van Eekelen, Daniil Frumin, Herman Geuvers +7
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verificati…
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…