issues
search
coq-community
/
coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
https://madiot.fr/coq100/
Other
55
stars
14
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
How to add a "new" theorem?
#38
Boutry
opened
7 months ago
1
Fix typos
#37
int-y1
closed
7 months ago
0
[birthday.v] use stdlib lemmas to prove collision_count and enumerate_no_collisions
#36
haansn08
opened
1 year ago
0
update CI with Coq 8.15 and 8.16, only use lower bound for Coq
#35
palmskog
closed
1 year ago
0
update locations of goedel and bertrand
#34
palmskog
closed
1 year ago
0
Add proof of 83, Friendship Theorem.
#33
aleloi
closed
1 year ago
0
Add proof of 59 and 62 by Avraham Shinnar and Barry Trager
#32
shinnar
closed
2 years ago
0
backwards-compatible fixes of deprecations in recent Coq
#31
palmskog
closed
2 years ago
0
consistent references to Lindemann repo for transcendence
#30
palmskog
closed
2 years ago
0
update Feuerbach reference and authors
#29
palmskog
closed
2 years ago
0
refresh ci configuration for 8.14, remove old boilerplate
#28
palmskog
closed
2 years ago
2
Fix coq-community references
#27
palmskog
closed
3 years ago
0
Metadata update after repo renaming
#26
palmskog
closed
3 years ago
0
Permalink to a more precise location for item 16?
#25
CohenCyril
closed
3 years ago
0
[Item 16] Abel - Ruffini Theorem
#24
CohenCyril
closed
3 years ago
2
add compatibility with Coq 8.13, update CI boilerplate
#23
palmskog
closed
3 years ago
0
Add formalization of problem 88
#22
FabianWolff
closed
3 years ago
3
Switch to GitHub Actions for CI
#21
palmskog
closed
3 years ago
0
fix contrib references, and some other obsolete links
#20
palmskog
closed
4 years ago
0
make all coq100 solutions refer to GitHub
#19
palmskog
closed
4 years ago
0
fix all Coqtail references
#18
palmskog
closed
4 years ago
4
fix URLs for all C-CoRN references
#17
palmskog
closed
4 years ago
0
fix references to qarith-stern-brocot and bertrand
#16
palmskog
closed
4 years ago
0
Linking to GitHub in index.html for hosted files
#15
palmskog
closed
4 years ago
1
Add link to Ptolemy's theorem
#14
palmskog
closed
4 years ago
0
Copyright notice update for cardan_ferrari.v
#13
fredericchardard
closed
4 years ago
0
Formalization of result 46 and update of result 37
#12
fredericchardard
closed
4 years ago
4
No code link for Ptolemy's theorem
#11
palmskog
closed
4 years ago
2
fix all deprecations on 8.12, including changing from omega to lia
#10
palmskog
closed
4 years ago
0
cardan3.v does not have a full proof of 37
#9
palmskog
closed
4 years ago
1
Separation of content from HTML file
#8
palmskog
opened
4 years ago
3
add metadata and generate boilerplate
#7
palmskog
closed
4 years ago
0
add _CoqProject and standard delegating Makefile
#6
palmskog
closed
4 years ago
0
Change name for this repository?
#5
jmadiot
closed
3 years ago
2
Consider moving this project to coq-community
#4
palmskog
closed
4 years ago
0
Added 78: Cauchy-Schwarz Inequality
#3
roglo
closed
7 years ago
0
Fix unicode characters in Puiseux' theorem statement.
#2
Zimmi48
closed
7 years ago
3
add some results contained in GeoCoq
#1
jnarboux
closed
8 years ago
2