|
|
|
|
|
|
by aziis98
165 days ago
|
|
|
The erdos problem website tells the theorem is formalized in Lean but on the mathlib project there is just the theorem statement with a sorry. Does someone know where I can find the lean proof? I don't know maybe it's in some random pull request I didn't find. Edit: Found it here https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/Er... |
|
|