issues
search
openai
/
miniF2F
Formal to Formal Mathematics Benchmark
309
stars
43
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Fix mathd_algebra_185
#77
DyeKuu
closed
2 years ago
0
Typo in mathd_algebra_247
#76
albertqjiang
closed
2 years ago
1
duplicate naming of assumptions in theorem mathd_numbertheory_405
#75
albertqjiang
closed
2 years ago
0
Missing constraint in amc12a_2013_p8
#74
albertqjiang
closed
2 years ago
2
Typo in theorem mathd_algebra_185?
#73
albertqjiang
closed
2 years ago
1
fix: amc12a_2017_p7
#72
spolu
closed
2 years ago
0
fix mathd-algebra-141
#71
DyeKuu
closed
2 years ago
1
complete mathd_algebra_141
#70
cuppajoeman
closed
2 years ago
1
Bump mathlib
#69
spolu
closed
2 years ago
0
prove mathd_algebra_484
#68
cuppajoeman
closed
2 years ago
1
prove mathd_numbertheory_229
#67
cuppajoeman
closed
2 years ago
3
Coq support?
#66
brando90
opened
2 years ago
41
prove: ∃ a b, irrational a ∧ irrational b ∧ ¬ irrational (a^b)
#65
cuppajoeman
closed
2 years ago
1
Fix formalization of mathd_algebra_13
#64
MantasBaksys
closed
2 years ago
1
Bump mathlib to 30a731ca565b92955e40274652f4c2b6f4db79f4
#63
spolu
closed
2 years ago
1
prove Induction sumkexp3eqsumksq
#62
cuppajoeman
closed
2 years ago
1
Possibility of updating lean/mathlib versions
#61
cuppajoeman
closed
2 years ago
2
add proof of induction_12dvd4expnp1p20
#60
cuppajoeman
closed
2 years ago
1
complete induction_nfactltnexpnm1ngt3
#59
cuppajoeman
closed
2 years ago
1
finish the proof of mathd_algebra_137
#58
cuppajoeman
closed
2 years ago
1
add one step to install instructions
#57
cuppajoeman
closed
2 years ago
1
Numbertheory 4x3m7y3neq2003
#56
cuppajoeman
closed
2 years ago
2
Add in some basic installation instructions
#55
cuppajoeman
closed
2 years ago
3
Project causes huge lag and tactic window doesn't load
#54
cuppajoeman
closed
2 years ago
2
add 330 HOL Light statements
#53
javier-m
closed
2 years ago
3
[Fix] Statement name mathd_numbertheory_133 -> 188
#52
DyeKuu
closed
2 years ago
1
Bump Lean/mathlib
#51
spolu
closed
3 years ago
2
Fix to IMO 1960 p2
#50
spolu
closed
3 years ago
1
README: add preprint bibtex
#49
spolu
closed
3 years ago
0
fix typo
#48
DyeKuu
closed
3 years ago
2
Lean aime_1988_p8
#47
TJ-Machado
closed
3 years ago
1
[lean] use a single {test,valid}.lean files
#46
spolu
closed
3 years ago
1
Updated README + Cut of v1
#45
spolu
closed
3 years ago
0
[Lean] fix name & ring_nf
#44
DyeKuu
closed
3 years ago
0
Fix duplicated statements
#43
DyeKuu
closed
3 years ago
0
[Metamath] Fix
#42
DyeKuu
closed
3 years ago
0
[Lean] Statements
#41
DyeKuu
closed
3 years ago
0
[Metamath] Fix typo in mathd-algebra-598.mm
#40
DyeKuu
closed
3 years ago
0
[Metamath] Statements
#39
DyeKuu
closed
3 years ago
1
[Lean & Metamath] fix statement
#38
DyeKuu
closed
3 years ago
0
More Isabelle data points for the test set
#37
Wenda302
closed
3 years ago
1
False theorem
#36
Wenda302
closed
3 years ago
1
[Lean] change Import
#35
DyeKuu
closed
3 years ago
1
[Lean] fix mathd_algebra_304
#34
DyeKuu
closed
3 years ago
0
bump mathlib
#33
spolu
closed
3 years ago
0
[Readme] Update
#32
DyeKuu
closed
3 years ago
1
[Readme] isabelle update
#31
DyeKuu
closed
3 years ago
1
[script] Lean linter & formatter
#30
DyeKuu
closed
3 years ago
1
Kudzo test
#29
Scikud
closed
3 years ago
3
[Isabelle] Initial data points from miniF2F_Isabelle
#28
Wenda302
closed
3 years ago
3
Previous
Next