Mathematics

2023

Cardinality and Representation of Stone Relation Algebras

by Walter Guttmann

Sep 22

Hypergraphs

by Chelsea Edmonds

Sep 20

General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma

by Chelsea Edmonds

Sep 20

General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma

by Chelsea Edmonds

Sep 20

Euler's Polyhedron Formula

by Lawrence C. Paulson

Sep 16

Ceva's Theorem

by Mathias Schack Rabing

Aug 16

Catoids, Categories, Groupoids

by Georg Struth

Aug 14

Catoids, Categories, Groupoids

by Georg Struth

Aug 14

Polygonal Number Theorem

by Kevin Lee, Zhengkun Ye and Angeliki Koutsoukou-Argyraki

Aug 10

Polygonal Number Theorem

by Kevin Lee, Zhengkun Ye and Angeliki Koutsoukou-Argyraki

Aug 10

Modal quantales, involutive quantales, Dedekind Quantales

by Georg Struth and Cameron Calk

Jul 25

Modal quantales, involutive quantales, Dedekind Quantales

by Georg Struth and Cameron Calk

Jul 25

Gray Codes for Arbitrary Numeral Systems

by Maximilian Spitz

Jul 11

Zeckendorf’s Theorem

by Christian Dalvit

Jun 12

Formalizing Results on Directed Sets

by Akihisa Yamada and Jérémy Dubut

May 24

Inner Structure, Determinism and Modal Algebra of Multirelations

by Walter Guttmann and Georg Struth

May 22

Tree Enumeration

by Nils Cremer

May 09

Tree Enumeration

by Nils Cremer

May 09

Three Squares Theorem

by Anton Danilkin and Loïc Chevalier

May 03

The Halting Problem is Soluble in Malament-Hogarth Spacetimes

by Mike Stannett

Apr 29

The Schwartz-Zippel Lemma

by Sunpill Kim and Yong Kiam Tan

Apr 27

The CHSH inequality: Tsirelson's upper-bound and other results

by Mnacho Echenim, Mehdi Mhalla and Coraline Mori

Apr 18

The CHSH inequality: Tsirelson's upper-bound and other results

by Mnacho Echenim, Mehdi Mhalla and Coraline Mori

Apr 18

Positional Notation for Natural Numbers in an Arbitrary Base

by Charles Staats

Apr 03

No Faster-Than-Light Observers (GenRel)

by Mike Stannett, Edward Higgins, Hajnal Andreka, Judit Madarasz, István Németi and Gergely Szekely

Mar 05

Expander Graphs

by Emin Karayel

Mar 03

A Sound and Complete Calculus for Probability Inequalities

by Matthew Doty

Feb 20

Group Law of Edwards Elliptic Curves

by Rodrigo Raya

Feb 16

Hardness of Lattice Problems

by Katharina Kreuzer

Feb 02

Suppes' Theorem For Probability Logic

by Matthew Doty

Jan 22

Strict Omega Categories

by Anthony Bordg and Adrián Doña Mateo

Jan 14

2022

Birkhoff's Representation Theorem For Finite Distributive Lattices

by Matthew Doty

Dec 06

Abstract Object Theory

by Daniel Kirchner

Nov 28

Sauer-Shelah Lemma

by Ata Keskin

Nov 24

Kneser's Theorem and the Cauchy–Davenport Theorem

by Mantas Bakšys and Angeliki Koutsoukou-Argyraki

Nov 21

Turán's Graph Theorem

by Nils Lauermann

Nov 14

The Balog–Szemerédi–Gowers Theorem

by Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds

Nov 11

The Balog–Szemerédi–Gowers Theorem

by Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds

Nov 11

Combinatorial Enumeration Algorithms

by Paul Hofmeier and Emin Karayel

Nov 11

The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections

by Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel and Patrick Lederer

Nov 10

Undirected Graph Theory

by Chelsea Edmonds

Sep 29

p-adic Fields and p-adic Semialgebraic Sets

by Aaron Crighton

Sep 22

p-adic Fields and p-adic Semialgebraic Sets

by Aaron Crighton

Sep 22

Risk-Free Lending

by Matthew Doty

Sep 18

The Hales–Jewett Theorem

by Ujkan Sulejmani, Manuel Eberl and Katharina Kreuzer

Sep 02

Khovanskii's Theorem

by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Sep 02

From THE BOOK: Two Squares via Involutions

by Maksym Bortin

Aug 15

Simultaneous diagonalization of pairwise commuting Hermitian matrices

by Mnacho Echenim

Jul 18

Pólya’s Proof of the Weighted Arithmetic–Geometric Mean Inequality

by Manuel Eberl

Jul 11

Finite Fields

by Emin Karayel

Jun 08

Diophantine Equations and the DPRM Theorem

by Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich and Dierk Schleicher

Jun 06

The Plünnecke-Ruzsa Inequality

by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

May 26

Clique is not solvable by monotone circuits of polynomial size

by René Thiemann

May 08

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics

by Chelsea Edmonds and Lawrence C. Paulson

Apr 21

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics

by Chelsea Edmonds and Lawrence C. Paulson

Apr 21

Digit Expansions

by Jonas Bayer, Marco David, Abhik Pal and Benedikt Stock

Apr 20

The Sophomore's Dream

by Manuel Eberl

Apr 10

Constructing the Reals as Dedekind Cuts of Rationals

by Jacques D. Fleuriot and Lawrence C. Paulson

Mar 24

A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent

by Manuel Eberl

Mar 15

Wetzel's Problem and the Continuum Hypothesis

by Lawrence C. Paulson

Feb 18

Enumeration of Equivalence Relations

by Emin Karayel

Feb 04

Quasi-Borel Spaces

by Michikazu Hirata, Yasuhiko Minamide and Tetsuya Sato

Feb 03

Duality of Linear Programming

by René Thiemann

Feb 03

Young's Inequality for Increasing Functions

by Lawrence C. Paulson

Jan 31

Interpolation Polynomials (in HOL-Algebra)

by Emin Karayel

Jan 29

Actuarial Mathematics

by Yosuke Ito

Jan 23

Irrational numbers from THE BOOK

by Lawrence C. Paulson

Jan 08

Knight's Tour Revisited Revisited

by Lukas Koller

Jan 04

2021

Hyperdual Numbers and Forward Differentiation

by Filip Smola and Jacques D. Fleuriot

Dec 31

Hyperdual Numbers and Forward Differentiation

by Filip Smola and Jacques D. Fleuriot

Dec 31

Gale-Shapley Algorithm

by Tobias Nipkow

Dec 29

Roth's Theorem on Arithmetic Progressions

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Dec 28

Roth's Theorem on Arithmetic Progressions

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Dec 28

Verified Algorithms for Solving Markov Decision Processes

by Maximilian Schäffeler and Mohammad Abdulaziz

Dec 16

Markov Decision Processes with Rewards

by Maximilian Schäffeler and Mohammad Abdulaziz

Dec 16

Simplicial Complexes and Boolean functions

by Jesús Aransay, Alejandro del Campo and Julius Michaelis

Nov 29

Foundation of geometry in planes, and some complements: Excluding the parallel axioms

by Fumiya Iwama

Nov 22

The Hahn and Jordan Decomposition Theorems

by Marie Cousin, Mnacho Echenim and Hervé Guiol

Nov 19

Real Exponents as the Limits of Sequences of Rational Exponents

by Jacques D. Fleuriot

Nov 08

Factorization of Polynomials with Algebraic Coefficients

by Manuel Eberl and René Thiemann

Nov 08

Szemerédi's Regularity Lemma

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Nov 05

Szemerédi's Regularity Lemma

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

Nov 05

Complex Bounded Operators

by José Manuel Rodríguez Caballero and Dominique Unruh

Sep 18

Category Theory for ZFC in HOL III: Universal Constructions

by Mihails Milehins

Sep 06

Category Theory for ZFC in HOL II: Elementary Theory of 1-Categories

by Mihails Milehins

Sep 06

Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

by Mihails Milehins

Sep 06

Solving Cubic and Quartic Equations

by René Thiemann

Sep 03

The Theorem of Three Circles

by Fox Thomson and Wenda Li

Aug 21

Combinatorial Design Theory

by Chelsea Edmonds and Lawrence C. Paulson

Aug 13

Relational Forests

by Walter Guttmann

Aug 03

Schutz' Independent Axioms for Minkowski Spacetime

by Richard Schmoetten, Jake Palmer and Jacques D. Fleuriot

Jul 27

Schutz' Independent Axioms for Minkowski Spacetime

by Richard Schmoetten, Jake Palmer and Jacques D. Fleuriot

Jul 27

Finitely Generated Abelian Groups

by Joseph Thommes and Manuel Eberl

Jul 07

Van der Waerden's Theorem

by Katharina Kreuzer and Manuel Eberl

Jun 22

Lifting the Exponent

by Maya Kądziołka

Apr 27

Gale-Stewart Games

by Sebastiaan J. C. Joosten

Apr 23

Grothendieck's Schemes in Algebraic Geometry

by Anthony Bordg, Lawrence C. Paulson and Wenda Li

Mar 29

Grothendieck's Schemes in Algebraic Geometry

by Anthony Bordg, Lawrence C. Paulson and Wenda Li

Mar 29

Hensel's Lemma for the p-adic Integers

by Aaron Crighton

Mar 23

Constructive Cryptography in HOL: the Communication Modeling Aspect

by Andreas Lochbihler and S. Reza Sefidgar

Mar 17

The Hermite–Lindemann–Weierstraß Transcendence Theorem

by Manuel Eberl

Mar 03

Quantum projective measurements and the CHSH inequality

by Mnacho Echenim

Mar 03

The Sunflower Lemma of Erdős and Rado

by René Thiemann

Feb 25

Formal Puiseux Series

by Manuel Eberl

Feb 17

The Laws of Large Numbers

by Manuel Eberl

Feb 10

Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid

by Roland Coghetto

Jan 31

2020

Cofinality and the Delta System Lemma

by Pedro Sánchez Terraf

Dec 27

Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information

by Anthony Bordg, Hanna Lachnitt and Yijun He

Nov 22

A Sound Type System for Physical Quantities, Units, and Measurements

by Simon Foster and Burkhart Wolff

Oct 20

Amicable Numbers

by Angeliki Koutsoukou-Argyraki

Aug 04

Ordinal Partitions

by Lawrence C. Paulson

Aug 03

Relational Characterisations of Paths

by Walter Guttmann and Peter Höfner

Jul 13

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

by Albert Rizaldi and Fabian Immler

Jun 01

A verified algorithm for computing the Smith normal form of a matrix

by Jose Divasón

May 23

The Nash-Williams Partition Theorem

by Lawrence C. Paulson

May 16

Irrationality Criteria for Series by Erdős and Straus

by Angeliki Koutsoukou-Argyraki and Wenda Li

May 12

Irrationality Criteria for Series by Erdős and Straus

by Angeliki Koutsoukou-Argyraki and Wenda Li

May 12

Banach-Steinhaus Theorem

by Dominique Unruh and José Manuel Rodríguez Caballero

May 02

The Lambert W Function on the Reals

by Manuel Eberl

Apr 24

Power Sum Polynomials

by Manuel Eberl

Apr 24

Gaussian Integers

by Manuel Eberl

Apr 24

Matrices for ODEs

by Jonathan Julian Huerta y Munive

Apr 19

Matrices for ODEs

by Jonathan Julian Huerta y Munive

Apr 19

Lucas's Theorem

by Chelsea Edmonds

Apr 07

Furstenberg's topology and his proof of the infinitude of primes

by Manuel Eberl

Mar 22

Arithmetic progressions and relative primes

by José Manuel Rodríguez Caballero

Feb 01

A Hierarchy of Algebras for Boolean Subsets

by Walter Guttmann and Bernhard Möller

Jan 31

Mersenne primes and the Lucas–Lehmer test

by Manuel Eberl

Jan 17

Bicategories

by Eugene W. Stark

Jan 06

2019

The Irrationality of ζ(3)

by Manuel Eberl

Dec 27

The Poincaré-Bendixson Theorem

by Fabian Immler and Yong Kiam Tan

Dec 18

Poincaré Disc Model

by Danijela Simić, Filip Marić and Pierre Boutry

Dec 16

Complex Geometry

by Filip Marić and Danijela Simić

Dec 16

Gauss Sums and the Pólya–Vinogradov Inequality

by Rodrigo Raya and Manuel Eberl

Dec 10

Verification Components for Hybrid Systems

by Jonathan Julian Huerta y Munive

Sep 10

Verification Components for Hybrid Systems

by Jonathan Julian Huerta y Munive

Sep 10

Fourier Series

by Lawrence C. Paulson

Sep 06

A Case Study in Basic Algebra

by Clemens Ballarin

Aug 30

Laplace Transform

by Fabian Immler

Aug 14

Linear Programming

by Julian Parsert and Cezary Kaliszyk

Aug 06

Communicating Concurrent Kleene Algebra for Distributed Systems Specification

by Maxime Buyse and Jason Jaskolka

Aug 06

Selected Problems from the International Mathematical Olympiad 2019

by Manuel Eberl

Aug 05

Order Extension and Szpilrajn's Extension Theorem

by Peter Zeller and Lukas Stevens

Jul 27

Complete Non-Orders and Fixed Points

by Akihisa Yamada and Jérémy Dubut

Jun 27

Linear Inequalities

by Ralph Bottesch, Alban Reynaud and René Thiemann

Jun 21

Hilbert's Nullstellensatz

by Alexander Maletzky

Jun 16

Hilbert's Nullstellensatz

by Alexander Maletzky

Jun 16

Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds

by Alexander Maletzky

Jun 15

The Transcendence of Certain Infinite Series

by Angeliki Koutsoukou-Argyraki and Wenda Li

Mar 27

The Transcendence of Certain Infinite Series

by Angeliki Koutsoukou-Argyraki and Wenda Li

Mar 27

Elementary Facts About the Distribution of Primes

by Manuel Eberl

Feb 21

Probabilistic Primality Testing

by Daniel Stüwe and Manuel Eberl

Feb 11

Farkas' Lemma and Motzkin's Transposition Theorem

by Ralph Bottesch, Max W. Haslbeck and René Thiemann

Jan 17

2018

Constructive Cryptography in HOL

by Andreas Lochbihler and S. Reza Sefidgar

Dec 17

Transformer Semantics

by Georg Struth

Dec 11

Quantales

by Georg Struth

Dec 11

Properties of Orderings and Lattices

by Georg Struth

Dec 11

Graph Saturation

by Sebastiaan J. C. Joosten

Nov 23

Matroids

by Jonas Keinholz

Nov 16

Smooth Manifolds

by Fabian Immler and Bohua Zhan

Oct 22

Smooth Manifolds

by Fabian Immler and Bohua Zhan

Oct 22

Upper Bounding Diameters of State Spaces of Factored Transition Systems

by Friedrich Kurz and Mohammad Abdulaziz

Oct 12

The Transcendence of π

by Manuel Eberl

Sep 28

Symmetric Polynomials

by Manuel Eberl

Sep 25

Signature-Based Gröbner Basis Algorithms

by Alexander Maletzky

Sep 20

The Prime Number Theorem

by Manuel Eberl and Lawrence C. Paulson

Sep 19

Aggregation Algebras

by Walter Guttmann

Sep 15

Octonions

by Angeliki Koutsoukou-Argyraki

Sep 14

Octonions

by Angeliki Koutsoukou-Argyraki

Sep 14

Quaternions

by Lawrence C. Paulson

Sep 05

Quaternions

by Lawrence C. Paulson

Sep 05

The Budan–Fourier Theorem and Counting Real Roots with Multiplicity

by Wenda Li

Sep 02

Pricing in discrete financial models

by Mnacho Echenim

Jul 16

Pricing in discrete financial models

by Mnacho Echenim

Jul 16

Von-Neumann-Morgenstern Utility Theorem

by Julian Parsert and Cezary Kaliszyk

Jul 04

Pell's Equation

by Manuel Eberl

Jun 23

The Localization of a Commutative Ring

by Anthony Bordg

Jun 14

Projective Geometry

by Anthony Bordg

Jun 14

Hidden Markov Models

by Simon Wimmer

May 25

Probabilistic Timed Automata

by Simon Wimmer and Johannes Hölzl

May 24

Irrational Rapidly Convergent Series

by Angeliki Koutsoukou-Argyraki and Wenda Li

May 23

Irrational Rapidly Convergent Series

by Angeliki Koutsoukou-Argyraki and Wenda Li

May 23

Axiom Systems for Category Theory in Free Logic

by Christoph Benzmüller and Dana Scott

May 23

The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

by Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker

Mar 22

The Error Function

by Manuel Eberl

Feb 06

A verified factorization algorithm for integer polynomials with polynomial complexity

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Feb 06

A verified LLL algorithm

by Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Feb 02

Gromov Hyperbolicity

by Sebastien Gouezel

Jan 16

An Isabelle/HOL formalisation of Green's Theorem

by Mohammad Abdulaziz and Lawrence C. Paulson

Jan 11

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

2017

The Falling Factorial of a Sum

by Lukas Bulwahn

Dec 22

The Mason–Stothers Theorem

by Manuel Eberl

Dec 21

Dirichlet L-Functions and Dirichlet's Theorem

by Manuel Eberl

Dec 21

Dirichlet L-Functions and Dirichlet's Theorem

by Manuel Eberl

Dec 21

Stochastic Matrices and the Perron-Frobenius Theorem

by René Thiemann

Nov 22

The Kuratowski Closure-Complement Theorem

by Peter Gammie and Gianpaolo Gioiosa

Oct 26

Evaluate Winding Numbers through Cauchy Indices

by Wenda Li

Oct 17

Count the Number of Complex Roots

by Wenda Li

Oct 17

Homogeneous Linear Diophantine Equations

by Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel

Oct 14

The Hurwitz and Riemann ζ Functions

by Manuel Eberl

Oct 12

The Hurwitz and Riemann ζ Functions

by Manuel Eberl

Oct 12

Linear Recurrences

by Manuel Eberl

Oct 12

Dirichlet Series

by Manuel Eberl

Oct 12

Microeconomics and the First Welfare Theorem

by Julian Parsert and Cezary Kaliszyk

Sep 01

Orbit-Stabiliser Theorem with Application to Rotational Symmetries

by Jonas Rädle

Aug 20

Stewart's Theorem and Apollonius' Theorem

by Lukas Bulwahn

Jul 31

Minkowski's Theorem

by Manuel Eberl

Jul 13

Minkowski's Theorem

by Manuel Eberl

Jul 13

Stone-Kleene Relation Algebras

by Walter Guttmann

Jul 06

Partial Semigroups and Convolution Algebras

by Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes and Georg Struth

Jun 13

Buffon's Needle Problem

by Manuel Eberl

Jun 06

Buffon's Needle Problem

by Manuel Eberl

Jun 06

Formalizing Push-Relabel Algorithms

by Peter Lammich and S. Reza Sefidgar

Jun 01

Flow Networks and the Min-Cut-Max-Flow Theorem

by Peter Lammich and S. Reza Sefidgar

Jun 01

Optics

by Simon Foster, Christian Pardillo-Laursen and Frank Zeyda

May 25

Probabilistic while loop

by Andreas Lochbihler

May 05

CryptHOL

by Andreas Lochbihler

May 05

Monoidal Categories

by Eugene W. Stark

May 04

Subresultants

by Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Apr 06

The Euler–MacLaurin Formula

by Manuel Eberl

Mar 10

Menger's Theorem

by Christoph Dittmann

Feb 26

Stone Relation Algebras

by Walter Guttmann

Feb 07

Bernoulli Numbers

by Lukas Bulwahn and Manuel Eberl

Jan 24

Bernoulli Numbers

by Lukas Bulwahn and Manuel Eberl

Jan 24

Bertrand's postulate

by Julian Biendarra and Manuel Eberl

Jan 17

The Transcendence of e

by Manuel Eberl

Jan 12

The Transcendence of e

by Manuel Eberl

Jan 12

2016

The Twelvefold Way

by Lukas Bulwahn

Dec 29

Expressiveness of Deep Learning

by Alexander Bentkamp

Nov 10

Stable Matching

by Peter Gammie

Oct 24

Source Coding Theorem

by Quentin Hibon and Lawrence C. Paulson

Oct 19

The Factorization Algorithm of Berlekamp and Zassenhaus

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Oct 14

Intersecting Chords Theorem

by Lukas Bulwahn

Oct 11

Lp spaces

by Sebastien Gouezel

Oct 05

Allen's Interval Calculus

by Fadoua Ghourabi

Sep 29

Stone Algebras

by Walter Guttmann

Sep 06

Stirling's formula

by Manuel Eberl

Sep 01

Ptolemy's Theorem

by Lukas Bulwahn

Aug 07

Chamber Complexes, Coxeter Systems, and Buildings

by Jeremy Sylvestre

Jul 01

Chamber Complexes, Coxeter Systems, and Buildings

by Jeremy Sylvestre

Jul 01

Category Theory with Adjunctions and Limits

by Eugene W. Stark

Jun 26

Cardinality of Multisets

by Lukas Bulwahn

Jun 26

Catalan Numbers

by Manuel Eberl

Jun 21

Program Construction and Verification Components Based on Kleene Algebra

by Victor B. F. Gomes and Georg Struth

Jun 18

Tree Decomposition

by Christoph Dittmann

May 31

Cardinality of Equivalence Relations

by Lukas Bulwahn

May 24

Perron-Frobenius Theorem for Spectral Radius Analysis

by Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada

May 20

A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks

by Andreas Lochbihler

May 09

Randomised Social Choice Theory

by Manuel Eberl

May 05

The Incompatibility of SD-Efficiency and SD-Strategy-Proofness

by Manuel Eberl

May 04

Spivey's Generalized Recurrence for Bell Numbers

by Lukas Bulwahn

May 04

Gröbner Bases Theory

by Fabian Immler and Alexander Maletzky

May 02

No Faster-Than-Light Observers

by Mike Stannett and István Németi

Apr 28

Kleene Algebras with Domain

by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber

Apr 12

The Cartan Fixed Point Theorems

by Lawrence C. Paulson

Mar 08

Polynomial Interpolation

by René Thiemann and Akihisa Yamada

Jan 29

Polynomial Factorization

by René Thiemann and Akihisa Yamada

Jan 29

Knot Theory

by T.V.H. Prathamesh

Jan 20

Tensor Product of Matrices

by T.V.H. Prathamesh

Jan 18

Cardinality of Number Partitions

by Lukas Bulwahn

Jan 14

2015

The Divergence of the Prime Harmonic Series

by Manuel Eberl

Dec 28

Liouville numbers

by Manuel Eberl

Dec 28

Liouville numbers

by Manuel Eberl

Dec 28

Descartes' Rule of Signs

by Manuel Eberl

Dec 28

Basic Geometric Properties of Triangles

by Manuel Eberl

Dec 28

The Stern-Brocot Tree

by Peter Gammie and Andreas Lochbihler

Dec 22

Algebraic Numbers in Isabelle/HOL

by René Thiemann, Akihisa Yamada and Sebastiaan J. C. Joosten

Dec 22

Cardinality of Set Partitions

by Lukas Bulwahn

Dec 12

Latin Square

by Alexander Bentkamp

Dec 02

Ergodic Theory

by Sebastien Gouezel

Dec 01

Euler's Partition Theorem

by Lukas Bulwahn

Nov 19

Planarity Certificates

by Lars Noschinski

Nov 11

Positional Determinacy of Parity Games

by Christoph Dittmann

Nov 02

Positional Determinacy of Parity Games

by Christoph Dittmann

Nov 02

Matrices, Jordan Normal Forms, and Spectral Radius Theory

by René Thiemann and Akihisa Yamada

Aug 21

Representations of Finite Groups

by Jeremy Sylvestre

Aug 12

The Akra-Bazzi theorem and the Master theorem

by Manuel Eberl

Jul 14

Landau Symbols

by Manuel Eberl

Jul 14

Hermite Normal Form

by Jose Divasón and Jesús Aransay

Jul 07

Derangements Formula

by Lukas Bulwahn

Jun 27

Binary Multirelations

by Hitoshi Furusawa and Georg Struth

Jun 11

VCG - Combinatorial Vickrey-Clarke-Groves Auctions

by Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat

Apr 30

Residuated Lattices

by Victor B. F. Gomes and Georg Struth

Apr 15

QR Decomposition

by Jose Divasón and Jesús Aransay

Feb 12

Echelon Form

by Jose Divasón and Jesús Aransay

Feb 12

2014

A Verified Compiler for Probability Density Functions

by Manuel Eberl, Johannes Hölzl and Tobias Nipkow

Oct 09

The Sturm–Tarski Theorem

by Wenda Li

Sep 19

The Cayley-Hamilton Theorem

by Stephan Adelsberger, Stefan Hetzl and Florian Pollak

Sep 15

The Jordan-Hölder Theorem

by Jakob von Raumer

Sep 09

Vector Spaces

by Holden Lee

Aug 29

Real-Valued Special Functions: Upper and Lower Bounds

by Lawrence C. Paulson

Aug 29

Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

by Peter Lammich

May 28

Regular Algebras

by Simon Foster and Georg Struth

May 21

Discrete Summation

by Florian Haftmann

Apr 13

Properties of Random Graphs -- Subgraph Containment

by Lars Hupel

Feb 13

Properties of Random Graphs -- Subgraph Containment

by Lars Hupel

Feb 13

Affine Arithmetic

by Fabian Immler

Feb 07

Implementing field extensions of the form Q[sqrt(b)]

by René Thiemann

Feb 06

Secondary Sylow Theorems

by Jakob von Raumer

Jan 28

Relation Algebra

by Alasdair Armstrong, Simon Foster, Georg Struth and Tjark Weber

Jan 25

Kleene Algebra with Tests and Demonic Refinement Algebras

by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

Jan 23

Sturm's Theorem

by Manuel Eberl

Jan 11

2013

Pratt's Primality Certificates

by Simon Wimmer and Lars Noschinski

Jul 22

Lehmer's Theorem

by Simon Wimmer and Lars Noschinski

Jul 22

The Königsberg Bridge Problem and the Friendship Theorem

by Wenda Li

Jul 19

An Axiomatic Characterization of the Single-Source Shortest Path Problem

by Christine Rizkallah

May 22

Graph Theory

by Lars Noschinski

Apr 28

Rank-Nullity Theorem in Linear Algebra

by Jose Divasón and Jesús Aransay

Jan 16

Kleene Algebra

by Alasdair Armstrong, Georg Struth and Tjark Weber

Jan 15

Computing N-th Roots using the Babylonian Method

by René Thiemann

Jan 03

2012

Open Induction

by Mizuhito Ogawa and Christian Sternagel

Nov 02

The independence of Tarski's Euclidean axiom

by T. J. M. Makarios

Oct 30

Bondy's Theorem

by Jeremy Avigad and Stefan Hetzl

Oct 27

Proving the Impossibility of Trisecting an Angle and Doubling the Cube

by Ralph Romanos and Lawrence C. Paulson

Aug 05

Proving the Impossibility of Trisecting an Angle and Doubling the Cube

by Ralph Romanos and Lawrence C. Paulson

Aug 05

Ordinary Differential Equations

by Fabian Immler and Johannes Hölzl

Apr 26

Well-Quasi-Orders

by Christian Sternagel

Apr 13

A Probabilistic Proof of the Girth-Chromatic Number Theorem

by Lars Noschinski

Feb 06

Markov Models

by Johannes Hölzl and Tobias Nipkow

Jan 03

2011

Pseudo Hoops

by George Georgescu, Laurentiu Leustean and Viorel Preoteasa

Sep 22

Lattice Properties

by Viorel Preoteasa

Sep 22

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

Aug 19

Maximum Cardinality Matching

by Christine Rizkallah

Jul 21

The General Triangle Is Unique

by Joachim Breitner

Apr 01

Lower Semicontinuous Functions

by Bogdan Grechuk

Jan 08

2010

Hall's Marriage Theorem

by Dongchen Jiang and Tobias Nipkow

Dec 17

Executable Multivariate Polynomials

by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp

Aug 10

Executable Multivariate Polynomials

by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp

Aug 10

Free Groups

by Joachim Breitner

Jun 24

Category Theory

by Alexander Katovsky

Jun 20

A Complete Proof of the Robbins Conjecture

by Matthew Doty

May 22

2009

Perfect Number Theorem

by Mark Ijbema

Nov 22

An Example of a Cofinitary Group in Isabelle/HOL

by Bart Kastermans

Aug 04

2008

Some classical results in Social Choice Theory

by Peter Gammie

Nov 09

Fun With Tilings

by Tobias Nipkow and Lawrence C. Paulson

Nov 07

Arrow and Gibbard-Satterthwaite

by Tobias Nipkow

Sep 01

Fun With Functions

by Tobias Nipkow

Aug 26

2007

Sums of Two and Four Squares

by Roelof Oosterhuis

Aug 12

Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples

by Roelof Oosterhuis

Aug 12

Fundamental Properties of Valuation Theory and Hensel's Lemma

by Hidetsune Kobayashi

Aug 08

2006

Flyspeck I: Tame Graphs

by Gertrud Bauer and Tobias Nipkow

May 22

Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality

by Benjamin Porter

Mar 14

2005

Category Theory to Yoneda's Lemma

by Greg O’Keefe

Apr 21

2004

Integration theory and random variables

by Stefan Richter

Nov 19

Ramsey's theorem, infinitary version

by Tom Ridge

Sep 20

Groups, Rings and Modules

by Hidetsune Kobayashi, L. Chen and H. Murao

May 18

Topology

by Stefan Friedrich

Apr 26