Related papers: Formalising perfectoid spaces
Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none…
In this paper we introduce a new kind of topological space, called 'structured space', which locally resembles various kinds of algebraic structures. This can be useful, for instance, to locally study a space that cannot be globally endowed…
The main objects of study are adic spaces with logarithmic structures. After establishing the basic definitions, we analyze the Kummer \'etale and pro-Kummer \'etale topologies on log adic spaces. In particular, we show that log adic spaces…
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.…
Pick's astonishing theorem explains how to obtain the area of any integer polygon by counting lattice points. It is a notoriously difficult challenge to translate the geometric statement and intuitive reasoning into a formal statement and…
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…
The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often,…
Before we can get the whole potential of employing computers in the process of managing mathematical `knowledge', we have to convert informal knowledge into machine-oriented representations. How exactly to support this process so that it…
We introduce the notion of scale to generalize and compare different invariants of metric spaces and their measures. Several versions of scales are introduced such as Hausdorff, packing, box, local and quantization. They moreover are…
We describe the formalization of the Ionescu-Tulcea theorem, showing the existence of a probability measure on the space of trajectories of a Markov chain, in the proof assistant Lean using the integrated library Mathlib. We first present a…
Mechanical reasoning is a key area of research that lies at the crossroads of mathematical logic and artificial intelligence. The main aim to develop mechanical reasoning systems (also known as theorem provers) was to enable mathematicians…
Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards developing a…
Large scale real number computation is an essential ingredient in several modern mathematical proofs. Because such lengthy computations cannot be verified by hand, some mathematicians want to use software proof assistants to verify the…
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis,…
We consider a generalized angle in complex normed vector spaces. Its definition corresponds to the definition of the well known Euclidean angle in real inner product spaces. Not surprisingly it yields complex values as `angles'. This…
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may…
The physics community relies on index notation to effectively manipulate types of tensors. This paper introduces the first formally verified implementation of index notation in the interactive theorem prover Lean 4. By integrating index…
We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library At Scale (Atlas) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task…
We study profinite completion of spaces in the model category of profinite spaces and construct a rigidification of the completion functors of Artin-Mazur and Sullivan which extends also to non-connected spaces. Another new aspect is an…
Regions-based theories of space aim -- among others -- to define points in a geometrically appealing way. The most famous definition of this kind is probably due to Whitehead. However, to conclude that the objects defined are points indeed,…