Mathematics/Algebra

Subject Classification

AMS: General algebraic systems

2023

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

Group Law of Edwards Elliptic Curves

by Rodrigo Raya

Feb 16

2022

Birkhoff's Representation Theorem For Finite Distributive Lattices

by Matthew Doty

Dec 06

p-adic Fields and p-adic Semialgebraic Sets

by Aaron Crighton

Sep 22

Simultaneous diagonalization of pairwise commuting Hermitian matrices

by Mnacho Echenim

Jul 18

Finite Fields

by Emin Karayel

Jun 08

Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics

by Chelsea Edmonds and Lawrence C. Paulson

Apr 21

Duality of Linear Programming

by René Thiemann

Feb 03

Interpolation Polynomials (in HOL-Algebra)

by Emin Karayel

Jan 29

2021

Hyperdual Numbers and Forward Differentiation

by Filip Smola and Jacques D. Fleuriot

Dec 31

Factorization of Polynomials with Algebraic Coefficients

by Manuel Eberl and René Thiemann

Nov 08

Finitely Generated Abelian Groups

by Joseph Thommes and Manuel Eberl

Jul 07

Grothendieck's Schemes in Algebraic Geometry

by Anthony Bordg, Lawrence C. Paulson and Wenda Li

Mar 29

Formal Puiseux Series

by Manuel Eberl

Feb 17

2020

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

by Jose Divasón

May 23

Power Sum Polynomials

by Manuel Eberl

Apr 24

Matrices for ODEs

by Jonathan Julian Huerta y Munive

Apr 19

A Hierarchy of Algebras for Boolean Subsets

by Walter Guttmann and Bernhard Möller

Jan 31

2019

Verification Components for Hybrid Systems

by Jonathan Julian Huerta y Munive

Sep 10

A Case Study in Basic Algebra

by Clemens Ballarin

Aug 30

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

Linear Inequalities

by Ralph Bottesch, Alban Reynaud and René Thiemann

Jun 21

Hilbert's Nullstellensatz

by Alexander Maletzky

Jun 16

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

by Alexander Maletzky

Jun 15

Farkas' Lemma and Motzkin's Transposition Theorem

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

Jan 17

2018

Transformer Semantics

by Georg Struth

Dec 11

Quantales

by Georg Struth

Dec 11

Symmetric Polynomials

by Manuel Eberl

Sep 25

Signature-Based Gröbner Basis Algorithms

by Alexander Maletzky

Sep 20

Aggregation Algebras

by Walter Guttmann

Sep 15

Octonions

by Angeliki Koutsoukou-Argyraki

Sep 14

Quaternions

by Lawrence C. Paulson

Sep 05

The Localization of a Commutative Ring

by Anthony Bordg

Jun 14

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

Taylor Models

by Christoph Traut and Fabian Immler

Jan 08

2017

The Mason–Stothers 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

Orbit-Stabiliser Theorem with Application to Rotational Symmetries

by Jonas Rädle

Aug 20

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

Optics

by Simon Foster, Christian Pardillo-Laursen and Frank Zeyda

May 25

Subresultants

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

Apr 06

Stone Relation Algebras

by Walter Guttmann

Feb 07

2016

The Factorization Algorithm of Berlekamp and Zassenhaus

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

Oct 14

Chamber Complexes, Coxeter Systems, and Buildings

by Jeremy Sylvestre

Jul 01

Program Construction and Verification Components Based on Kleene Algebra

by Victor B. F. Gomes and Georg Struth

Jun 18

Perron-Frobenius Theorem for Spectral Radius Analysis

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

May 20

Gröbner Bases Theory

by Fabian Immler and Alexander Maletzky

May 02

Kleene Algebras with Domain

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

Apr 12

Polynomial Interpolation

by René Thiemann and Akihisa Yamada

Jan 29

Polynomial Factorization

by René Thiemann and Akihisa Yamada

Jan 29

Tensor Product of Matrices

by T.V.H. Prathamesh

Jan 18

2015

Algebraic Numbers in Isabelle/HOL

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

Dec 22

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

Hermite Normal Form

by Jose Divasón and Jesús Aransay

Jul 07

Binary Multirelations

by Hitoshi Furusawa and Georg Struth

Jun 11

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

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

Regular Algebras

by Simon Foster and Georg Struth

May 21

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

2013

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

2012

Proving the Impossibility of Trisecting an Angle and Doubling the Cube

by Ralph Romanos and Lawrence C. Paulson

Aug 05

2011

Pseudo Hoops

by George Georgescu, Laurentiu Leustean and Viorel Preoteasa

Sep 22

Gauss-Jordan Elimination for Matrices Represented as Functions

by Tobias Nipkow

Aug 19

2010

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

A Complete Proof of the Robbins Conjecture

by Matthew Doty

May 22

2009

An Example of a Cofinitary Group in Isabelle/HOL

by Bart Kastermans

Aug 04

2007

Fundamental Properties of Valuation Theory and Hensel's Lemma

by Hidetsune Kobayashi

Aug 08

2004

Groups, Rings and Modules

by Hidetsune Kobayashi, L. Chen and H. Murao

May 18