Cover Image

A complete formalization of Fermat's Last Theorem for regular primes in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Best, Alex, Birkbeck, Christopher, Brasca, Riccardo, Boidi, Eric Rodriguez, van De Velde, Ruben, Yang, Andrew
Format:	Preprint
Published:	2024
Subjects:	Formal Languages and Automata Theory Logic in Computer Science Number Theory
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing zeta and L-functions in Lean
by: Loeffler, David, et al.
Published: (2025)

Categorical Foundations of Formalized Condensed Mathematics
by: Asgeirsson, Dagur, et al.
Published: (2024)

Beatty Sequences for a Quadratic Irrational: Decidability and Applications
by: Schaeffer, Luke, et al.
Published: (2024)

An algebraic theory of ω-regular languages, via μν-expressions
by: Das, Anupam, et al.
Published: (2025)

Parikh's Theorem Made Symbolic
by: Hague, Matthew, et al.
Published: (2023)

Algebraic power series and their automatic complexity modulo prime powers
by: Rowland, Eric, et al.
Published: (2024)

A Dichotomy Theorem for Automatic Structures
by: Cuvelier, Antoine, et al.
Published: (2026)

A Completeness Theorem for Probabilistic Regular Expressions
by: Różowski, Wojciech, et al.
Published: (2023)

Some properties of $β$-$η$-normal forms in $λ$-K-calculus (Alcune proprietá delle forme $β$-$η$-normali nel $λ$-K-calcolo)
by: Böhm, Corrado, et al.
Published: (2025)

First-Order Intuitionistic Linear Logic and Hypergraph Languages
by: Pshenitsyn, Tikhon
Published: (2025)

A Diamond Structure in the Transducer Hierarchy
by: Kaufmann, Noah
Published: (2021)

Word equations, constraints, and formal languages
by: Ciobanu, Laura
Published: (2024)

A formal characterization of discrete condensed objects
by: Asgeirsson, Dagur
Published: (2024)

Equations in wreath products
by: Bartholdi, Laurent, et al.
Published: (2024)

A cartesian closed fibration of higher-order regular languages
by: Melliès, Paul-André, et al.
Published: (2026)

Learning Verified Monitors for Hidden Markov Models
by: van der Maas, Luko, et al.
Published: (2025)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
by: Guan, Naillin, et al.
Published: (2025)

Generalized Hofstadter functions $G, H$ and beyond: numeration systems and discrepancy
by: Letouzey, Pierre
Published: (2025)

A formal query language and automata model for aggregation in complex event recognition
by: Bourhis, Pierre, et al.
Published: (2026)

Robust Probabilistic Bisimilarity for Labelled Markov Chains
by: Fatmi, Syyeda Zainab, et al.
Published: (2025)

Complex event recognition under time constraints: towards a formal framework for efficient query evaluation
by: García, Julián, et al.
Published: (2025)

Proving Properties of $φ$-Representations with the Walnut Theorem-Prover
by: Shallit, Jeffrey
Published: (2023)

A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
by: Rooduijn, Jan, et al.
Published: (2024)

A proof theory of right-linear (omega-)grammars via cyclic proofs
by: Das, Anupam, et al.
Published: (2024)

The Alternation Hierarchy of First-Order Logic on Words is Decidable
by: Barloy, Corentin, et al.
Published: (2025)

Positive First-order Logic on Words and Graphs
by: Kuperberg, Denis
Published: (2022)

Function spaces for orbit-finite sets
by: Bojańczyk, Mikołaj, et al.
Published: (2024)

An efficient quantifier elimination procedure for Presburger arithmetic
by: Haase, Christoph, et al.
Published: (2024)

Cyclic system for an algebraic theory of alternating parity automata
by: Das, Anupam, et al.
Published: (2025)

New properties of the $φ$-representation of integers
by: Shallit, Jeffrey, et al.
Published: (2025)

S-unit equations in modules and linear-exponential Diophantine equations
by: Dong, Ruiwen, et al.
Published: (2025)

A Sharper Upper Bound for the Separating Words Problem
by: Dumitru, Bogdan C.
Published: (2025)

Completing the picture for the Skolem Problem on order-4 linear recurrence sequences
by: Bacik, Piotr
Published: (2024)

Recursive Prime Factorizations: Dyck Words as Numbers
by: Childress, Ralph L.
Published: (2021)

The commutativity problem for effective varieties of formal series, and applications
by: Clemente, Lorenzo
Published: (2025)

Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
by: Abdulla, Parosh Aziz, et al.
Published: (2024)

The Queue Automaton Revisited
by: Baeten, Jos C. M., et al.
Published: (2025)

Relating Reversible Petri Nets and Reversible Event Structures, categorically
by: Melgratti, Hernán, et al.
Published: (2023)

Simplifying LTL Model Checking Given Prior Knowledge
by: Duret-Lutz, Alexandre, et al.
Published: (2025)

Determinization of Min-Plus Weighted Automata is Decidable
by: Almagor, Shaull, et al.
Published: (2025)