This paper outlines the formalization of derived categories in the mathematical library of the proof assistant Lean 4. The derived category D(C) of any abelian category C is formalized as the localization of the category of unbounded cochain complexes with respect to the class of quasi-isomorphisms, and it is endowed with a triangulated structure.
The Riemann zeta function, and more generally the L-functions of Dirichlet characters, are among the central objects of study in number theory. We report on a project to formalize the theory of these objects in Lean's "Mathlib" library, including a proof of Dirichlet's theorem on primes in arithmetic progressions and a formal statement of the Riemann hypothesis
Derandomization techniques are often used within advanced randomized algorithms. In particular, pseudorandom objects, such as hash families and expander graphs, are key components of such algorithms, but their verification presents a challenge. This work shows how such algorithms can be expressed and verified in Isabelle and presents a pseudorandom objects library that abstracts away the deep algebraic/analytic results involved. Moreover, it presents examples that show how the library eases and enables the verification of advanced randomized algorithms. Highlighting the value of this framework is that it was recently used to verify the space-optimal distinct elements algorithm by Blasiok from 2018, which relies on the combination of many derandomization techniques to achieve its optimality.
We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formalization.
The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why. We describe a formal proof that the adele ring of a number field is locally compact implemented in the Lean 4 theorem prover. Our work includes the formalisations of new types, including the completion of a number field at an infinite place, the infinite adele ring and the finite $S$-adele ring, as well as formal proofs that completions of a number field are locally compact and that their rings of integers at finite places are compact.
