Related papers: A Formalised Theorem in the Partition Calculus
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$.…
We introduce the linear operators of fractional integration and fractional differentiation in the framework of the Riemann-Liouville fractional calculus. Particular attention is devoted to the technique of Laplace transforms for treating…
We consider a class of $n^{\text{th}}$-order linear ordinary differential equations with a large parameter $u$. Analytic solutions of these equations can be described by (divergent) formal series in descending powers of $u$. We demonstrate…
The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration…
The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every…
G\"odel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction…
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method.…
The aim of this paper is to prove all well-known metrization theorems using partitions of unity. To accomplish this, we first discuss sufficient and necessary conditions for existence of $\mathcal{U}$-small partitions of unity (partitions…
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and…
We describe an experiment in LLM-assisted autoformalization that produced over 85,000 lines of Isabelle/HOL code covering all 39 sections of Munkres' Topology (general topology, Chapters 2--8), from topological spaces through dimension…
We propose an epistemic approach to formalizing statistical properties of machine learning. Specifically, we introduce a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible…
I use mechanized verification to examine several first- and higher-order formalizations of Anselm's Ontological Argument against the charge of begging the question. I propose three different but related criteria for a premise to beg the…
The discussion regarding the numerical integration of the polarized radiative transfer equation is still open and the comparison between the different numerical schemes proposed by different authors in the past is not fully clear. Aiming at…
We present a characterization of the completeness of the field of real numbers in the form of a \emph{collection of several equivalent statements} borrowed from algebra, real analysis, general topology, and non-standard analysis. We also…
Complex systems (CS) are ubiquitous in nature. It is argued that fractional order (FO) calculus is more suitable to describe fractal systems. Motivated by the fractal space time theory some fractional generalizations of Scrodinger and…
We formalise the basics of the double-pushout approach to graph transformation in the proof assistant Isabelle/HOL and provide associated machine-checked proofs. Specifically, we formalise graphs, graph morphisms and rules, and a definition…
The theory of finitely supported algebraic structures is related to Pitts theory of nominal sets (by equipping finitely supported sets with finitely supported internal algebraic laws). It represents a reformulation of Zermelo Fraenkel set…
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal…
The theory of finitely supported algebraic structures represents a reformulation of Zermelo-Fraenkel set theory in which every construction is finitely supported according to the action of a group of permutations of some basic elements…
Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using…