issues
search
jesse-michael-han
/
lean-gptf
Interactive neural theorem proving in Lean
Apache License 2.0
118
stars
6
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Is there any version for Lean 4?
#13
EricZhongYJ
opened
11 months ago
1
It seems that the model "formal-lean-pact" doesn't exist.
#12
venom12138
opened
2 years ago
0
Getting Invalid Organization error
#11
saisurbehera
opened
2 years ago
3
chore(): bump mathlib + Lean version
#10
Julian
closed
2 years ago
0
chore(bump mathlib)
#9
spolu
closed
3 years ago
0
OpenAI key
#8
ayush1801
opened
3 years ago
1
bump to Lean 3.31.0
#7
ericrbg
closed
3 years ago
2
chore(bump Lean version)
#6
spolu
closed
3 years ago
0
chore(bump Lean version)
#5
spolu
closed
3 years ago
2
feat(tactic/gptf/utils/util) JSON escape double quotes
#4
alexjbest
closed
3 years ago
1
feat(tactic/gptf/backends/openai) add no buffer flag to curl
#3
alexjbest
closed
3 years ago
1
More care should be taken escaping json (on Windows at least)
#2
alexjbest
closed
3 years ago
0
fix(tactic/gptf/backends/openai): detect windows and escape json for `curl`
#1
alexjbest
closed
3 years ago
1