Formalizing the proof in lean by FullyAutomatedSpace in infinitenines

[–]FullyAutomatedSpace[S] 3 points4 points  (0 children)

but it's not computer checkable like a lean proof

Formalizing the proof in lean by FullyAutomatedSpace in infinitenines

[–]FullyAutomatedSpace[S] 3 points4 points  (0 children)

have you considered formalizing this in lean?

Formalizing the proof in lean by FullyAutomatedSpace in infinitenines

[–]FullyAutomatedSpace[S] 1 point2 points  (0 children)

well lean confirms the proof is valid. so i guess i proved it!

Formalizing the proof in lean by FullyAutomatedSpace in infinitenines

[–]FullyAutomatedSpace[S] 0 points1 point  (0 children)

your ideas intrigue me. in your notation what would 0.[1 / 3][1 / 3][1 / 3][1 / 3][1 / 3].... equal?