| Publication | Date of Publication | Type |
|---|
Elementary number theory problems. XIX
Formalized Mathematics | 2026-03-23 | Paper |
Conway's normal form in the Mizar system
Formalized Mathematics | 2026-02-12 | Paper |
Surreal dyadic and real numbers: a formal construction
Formalized Mathematics | 2026-02-12 | Paper |
Surreal numbers: a study of square roots
Formalized Mathematics | 2026-02-12 | Paper |
| Conway normal form: bridging approaches for comprehensive formalization of surreal numbers | 2026-02-10 | Paper |
Elementary number theory problems. XVI
Formalized Mathematics | 2025-06-30 | Paper |
Elementary number theory problems. Part XV: Diophantine equations
Formalized Mathematics | 2025-06-30 | Paper |
Inverse element for surreal number
Formalized Mathematics | 2025-06-30 | Paper |
| Formalizing a Diophantine representation of the set of prime numbers | 2024-07-15 | Paper |
Conway numbers -- formal introduction
Formalized Mathematics | 2024-06-18 | Paper |
Integration of game theoretic and tree theoretic approaches to Conway numbers
Formalized Mathematics | 2024-06-18 | Paper |
The ring of Conway numbers in Mizar
Formalized Mathematics | 2024-06-18 | Paper |
Prime representing polynomial with 10 unknowns -- introduction. II
Formalized Mathematics | 2024-06-18 | Paper |
Prime representing polynomial with 10 unknowns
Formalized Mathematics | 2024-06-18 | Paper |
Prime representing polynomial with 10 unknowns -- introduction
Formalized Mathematics | 2024-04-22 | Paper |
Combining higher-order logic with set theory formalizations
Journal of Automated Reasoning | 2023-06-27 | Paper |
| Declarative Proof Translation (Short Paper) | 2023-02-03 | Paper |
| Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. | 2023-02-03 | Paper |
Prime representing polynomial
Formalized Mathematics | 2022-09-09 | Paper |
| Formalizing a Diophantine Representation of the Set of Prime Numbers | 2022-04-26 | Paper |
Grothendieck universes
Formalized Mathematics | 2022-03-14 | Paper |
AIM loops and the AIM conjecture
Formalized Mathematics | 2020-03-10 | Paper |
A tale of two set theories
(available as arXiv preprint) | 2020-01-22 | Paper |
Diophantine sets. II
Formalized Mathematics | 2019-11-19 | Paper |
Formalization of the MRDP theorem in the Mizar system
Formalized Mathematics | 2019-11-19 | Paper |
Semantics of Mizar as an Isabelle object logic
Journal of Automated Reasoning | 2019-09-02 | Paper |
Basic Diophantine relations
Formalized Mathematics | 2019-07-10 | Paper |
Isabelle formalization of set theoretic structures and set comprehensions
Mathematical Aspects of Computer and Information Sciences | 2019-03-14 | Paper |
| Isabelle import infrastructure for the Mizar Mathematical Library | 2018-10-18 | Paper |
Diophantine sets. Preliminaries
Formalized Mathematics | 2018-10-17 | Paper |
The Matiyasevich theorem. Preliminaries
Formalized Mathematics | 2018-10-16 | Paper |
The role of the Mizar mathematical library for interactive proof development in Mizar
Journal of Automated Reasoning | 2018-08-21 | Paper |
Pell's equation
Formalized Mathematics | 2018-01-11 | Paper |
Basel problem -- preliminaries
Formalized Mathematics | 2017-10-06 | Paper |
Basel problem
Formalized Mathematics | 2017-10-06 | Paper |
Vieta's formula about the sum of roots of polynomials
Formalized Mathematics | 2017-10-06 | Paper |
| Presentation and manipulation of Mizar properties in an Isabelle object logic | 2017-07-21 | Paper |
Leibniz series for
Formalized Mathematics | 2017-04-03 | Paper |
Bertrand's ballot theorem
Formalized Mathematics | 2017-01-06 | Paper |
Topological manifolds
Formalized Mathematics | 2017-01-06 | Paper |
Improving legibility of formal proofs based on the close reference principle is NP-hard
Journal of Automated Reasoning | 2016-05-26 | Paper |
Mizar: state-of-the-art and beyond
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Readable formalization of Euler's partition theorem in Mizar
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Flexary operations
Formalized Mathematics | 2015-08-19 | Paper |
Euler's partition theorem
Formalized Mathematics | 2015-08-19 | Paper |
Tietze extension theorem for n-dimensional spaces
Formalized Mathematics | 2014-11-05 | Paper |
Brouwer invariance of domain theorem
Formalized Mathematics | 2014-11-05 | Paper |
Improving legibility of natural deduction proofs is not trivial
Logical Methods in Computer Science | 2014-09-30 | Paper |
Automated Improving of Proof Legibility in the Mizar System
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Continuity of barycentric coordinates in Euclidean topological spaces
Formalized Mathematics | 2013-12-03 | Paper |
The rotation group
Formalized Mathematics | 2013-12-03 | Paper |
Linear transformations of Euclidean topological spaces
Formalized Mathematics | 2013-12-03 | Paper |
Linear transformations of Euclidean topological spaces. II.
Formalized Mathematics | 2013-12-03 | Paper |
Brouwer fixed point theorem for simplexes
Formalized Mathematics | 2013-12-03 | Paper |
Brouwer fixed point theorem in the general case
Formalized Mathematics | 2013-12-03 | Paper |
The friendship theorem
Formalized Mathematics | 2013-10-08 | Paper |
Methods of lemma extraction in natural deduction proofs
Journal of Automated Reasoning | 2013-04-17 | Paper |
