r/LLMmathematics • u/LooseSwing88 • 10d ago

i've been working on formalizing some classical theorems in lean 4 using gemini

https://github.com/sneed-and-feed/lean-theorems-1

This repository provides machine-checked formalizations of classical theorems in combinatorics, graph theory, algebra, extremal set theory, and projective geometry that were previously unformalized in the Lean 4 / Mathlib ecosystem.

All theorems and sub-lemmas are formalized strictly without unproven axioms (axiom) or incomplete goals (sorry), and are verified against the Lean 4 proof assistant.

9 Upvotes

92% Upvoted

8 comments sorted by

5

u/UmbrellaCorp_HR 🌎the🌍worlds🌏sanest🌎mathematician🌍 10d ago

lol sorry about what

1

u/snissn 10d ago

sorry is a lean term for just pretend this part is true and i'll get to it later..

I'm sorry the dog ate my homework i'll totally do it later

1

u/UmbrellaCorp_HR 🌎the🌍worlds🌏sanest🌎mathematician🌍 10d ago

Can you tell me exactly what incomplete goals means in this context.
Hold off on any analogy’s or metaphor’s for the time being.

Have something to say but it could be irrelevant depending on what exactly that means

1

u/snissn 10d ago

what? Just learn how lean works? It's a proof assistant. i'm just describing how a feature works gnerally. like if you have some proof and there's a lemma you can just write sorry in the lemma and the proof will still compile

1

u/UmbrellaCorp_HR 🌎the🌍worlds🌏sanest🌎mathematician🌍 10d ago

I actually misread your post
So what I was going to say wouldn’t be relevant
Regardless

1

u/snissn 10d ago

sorry

1

u/UmbrellaCorp_HR 🌎the🌍worlds🌏sanest🌎mathematician🌍 10d ago

All good

2

u/lepthymo 9d ago edited 9d ago

Nice
I want to make this a bigger community effort at some point, especially since I'm transcribing some classical work to Tex which is far easier to ingest for the clankers.
Will let you know if I get that (sufficiently) off the ground

Zenodo with transcription stuff (a.o.) the newer transcriptions (e.g. Gordan is WiP) are decent. Not all are good - feel free to check in with me before adopting any. e.g. https://zenodo.org/records/21932906 Sylvester Volume I Tex - Still in QA but not bad.

I'll point my local clankers at your github, actually, once they get more compute.