Abel

Galois theorem formalizer

Formalization of mathematical theorems about solvability and Galois theory for polynomials

A proof of Abel-Ruffini theorem.

GitHub

28 stars

8 watching

8 forks

Language: Coq

last commit: almost 2 years ago

abel-ruffinicoqgalois-theorymathcompssreflect

Related projects:

Repository	Description	Stars
math-comp/coq-combi	Formalizes algebraic combinatorics and symmetric functions in Coq.	37
math-comp/math-comp	A comprehensive library of formalized mathematical theories	593
thery/mathcomp-extra	A collection of reusable mathematical components and algorithms implemented in Coq	5
math-comp/odd-order	Verifies a mathematical theorem in finite group theory	27
affeldt-aist/infotheo	A formalization of information theory and linear error-correcting codes in Coq.	64
stepchowfun/proofs	A personal repository of formally verified mathematics using the Coq proof assistant	292
math-comp/analysis	A Coq proof-assistant library for real analysis and mathematical structures	210
vafeiadis/hahn	A collection of lemmas and tactics about lists and binary relations for a proof assistant	30
charguer/tlc	A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems.	38
coq-community/lemma-overloading	A Coq library demonstrating design patterns for automated proof automation and canonical structures	26
ilyasergey/pnp	A tutorial project on using Coq to mechanize mathematics with dependent types	160
llee454/functional-algebra	A Coq formalization of abstract algebra using functional programming style	28
coq-community/coqtail-math	A collection of mathematical theorems and tools within the Coq proof assistant	15
geohot/coq-hardy	Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory	53
coq-community/gaia	A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics	30