Mathematics/Algebra

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics
by Chelsea Edmonds and Lawrence C. Paulson

Duality of Linear Programming
by René Thiemann

Interpolation Polynomials (in HOL-Algebra)
by Emin Karayel

Hyperdual Numbers and Forward Differentiation
by Filip Smola and Jacques Fleuriot

Factorization of Polynomials with Algebraic Coefficients
by Manuel Eberl and René Thiemann

Finitely Generated Abelian Groups
by Joseph Thommes and Manuel Eberl

Grothendieck's Schemes in Algebraic Geometry
by Anthony Bordg, Lawrence C. Paulson and Wenda Li

Formal Puiseux Series
by Manuel Eberl

A verified algorithm for computing the Smith normal form of a matrix
by Jose Divasón

Power Sum Polynomials
by Manuel Eberl

Matrices for ODEs
by Jonathan Julian Huerta y Munive

A Hierarchy of Algebras for Boolean Subsets
by Walter Guttmann and Bernhard Möller

Verification Components for Hybrid Systems
by Jonathan Julian Huerta y Munive

A Case Study in Basic Algebra
by Clemens Ballarin

Linear Programming
by Julian Parsert and Cezary Kaliszyk

Communicating Concurrent Kleene Algebra for Distributed Systems Specification
by Maxime Buyse and Jason Jaskolka

Linear Inequalities
by Ralph Bottesch, Alban Reynaud and René Thiemann

Hilbert's Nullstellensatz
by Alexander Maletzky

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

Farkas' Lemma and Motzkin's Transposition Theorem
by Ralph Bottesch, Max W. Haslbeck and René Thiemann

Transformer Semantics
by Georg Struth

Quantales
by Georg Struth

Symmetric Polynomials
by Manuel Eberl

Signature-Based Gröbner Basis Algorithms
by Alexander Maletzky

Aggregation Algebras
by Walter Guttmann

Octonions
by Angeliki Koutsoukou-Argyraki

Quaternions
by Lawrence C. Paulson

The Localization of a Commutative Ring
by Anthony Bordg

A verified factorization algorithm for integer polynomials with polynomial complexity
by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

A verified LLL algorithm
by Ralph Bottesch, Jose Divasón, Maximilian P. L. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Taylor Models
by Christoph Traut and Fabian Immler

The Mason–Stothers Theorem
by Manuel Eberl

Dirichlet L-Functions and Dirichlet's Theorem
by Manuel Eberl

Stochastic Matrices and the Perron-Frobenius Theorem
by René Thiemann

Orbit-Stabiliser Theorem with Application to Rotational Symmetries
by Jonas Rädle

Stone-Kleene Relation Algebras
by Walter Guttmann

Partial Semigroups and Convolution Algebras
by Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes and Georg Struth

Optics
by Simon Foster and Frank Zeyda

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

Stone Relation Algebras
by Walter Guttmann

The Factorization Algorithm of Berlekamp and Zassenhaus
by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Chamber Complexes, Coxeter Systems, and Buildings
by Jeremy Sylvestre

Program Construction and Verification Components Based on Kleene Algebra
by Victor B. F. Gomes and Georg Struth

Perron-Frobenius Theorem for Spectral Radius Analysis
by Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada

Gröbner Bases Theory
by Fabian Immler and Alexander Maletzky

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

Polynomial Interpolation
by René Thiemann and Akihisa Yamada

Polynomial Factorization
by René Thiemann and Akihisa Yamada

Tensor Product of Matrices
by T.V.H. Prathamesh

Algebraic Numbers in Isabelle/HOL
by René Thiemann, Akihisa Yamada and Sebastiaan J. C. Joosten

Matrices, Jordan Normal Forms, and Spectral Radius Theory
by René Thiemann and Akihisa Yamada

Representations of Finite Groups
by Jeremy Sylvestre

Hermite Normal Form
by Jose Divasón and Jesús Aransay

Binary Multirelations
by Hitoshi Furusawa and Georg Struth

Residuated Lattices
by Victor B. F. Gomes and Georg Struth

QR Decomposition
by Jose Divasón and Jesús Aransay

Echelon Form
by Jose Divasón and Jesús Aransay

The Cayley-Hamilton Theorem
by Stephan Adelsberger, Stefan Hetzl and Florian Pollak

The Jordan-Hölder Theorem
by Jakob von Raumer

Vector Spaces
by Holden Lee

Regular Algebras
by Simon Foster and Georg Struth

Secondary Sylow Theorems
by Jakob von Raumer

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

Kleene Algebra with Tests and Demonic Refinement Algebras
by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

Rank-Nullity Theorem in Linear Algebra
by Jose Divasón and Jesús Aransay

Kleene Algebra
by Alasdair Armstrong, Georg Struth and Tjark Weber

Proving the Impossibility of Trisecting an Angle and Doubling the Cube
by Ralph Romanos and Lawrence C. Paulson

Pseudo Hoops
by George Georgescu, Laurentiu Leustean and Viorel Preoteasa

Gauss-Jordan Elimination for Matrices Represented as Functions
by Tobias Nipkow

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

Free Groups
by Joachim Breitner

A Complete Proof of the Robbins Conjecture
by Matthew Wampler-Doty

An Example of a Cofinitary Group in Isabelle/HOL
by Bart Kastermans

Fundamental Properties of Valuation Theory and Hensel's Lemma
by Hidetsune Kobayashi

Groups, Rings and Modules
by Hidetsune Kobayashi, L. Chen and H. Murao