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: 2 months 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