Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics

by Chelsea Edmonds and Lawrence C. Paulson

# Mathematics/Algebra

## 2022

## 2021

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

## 2020

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

by Jose Divasón

A Hierarchy of Algebras for Boolean Subsets

by Walter Guttmann and Bernhard Möller

## 2019

Verification Components for Hybrid Systems

by Jonathan Julian Huerta y Munive

Communicating Concurrent Kleene Algebra for Distributed Systems Specification

by Maxime Buyse and Jason Jaskolka

Linear Inequalities

by Ralph Bottesch, Alban Reynaud and René Thiemann

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

## 2018

Signature-Based Gröbner Basis Algorithms

by Alexander Maletzky

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

## 2017

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

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

## 2016

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

Kleene Algebras with Domain

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

## 2015

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

## 2014

The Cayley-Hamilton Theorem

by Stephan Adelsberger, Stefan Hetzl and Florian Pollak

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

## 2013

Rank-Nullity Theorem in Linear Algebra

by Jose Divasón and Jesús Aransay

Kleene Algebra

by Alasdair Armstrong, Georg Struth and Tjark Weber

## 2012

Proving the Impossibility of Trisecting an Angle and Doubling the Cube

by Ralph Romanos and Lawrence C. Paulson

## 2011

Pseudo Hoops

by George Georgescu, Laurentiu Leustean and Viorel Preoteasa

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

## 2010

Executable Multivariate Polynomials

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

A Complete Proof of the Robbins Conjecture

by Matthew Wampler-Doty

## 2009

An Example of a Cofinitary Group in Isabelle/HOL

by Bart Kastermans

## 2007

Fundamental Properties of Valuation Theory and Hensel's Lemma

by Hidetsune Kobayashi

## 2004

Groups, Rings and Modules

by Hidetsune Kobayashi, L. Chen and H. Murao