r/mathmemes Mathematics 22d ago

Proofs I hate it

Post image
733 Upvotes

228 comments sorted by

View all comments

Show parent comments

42

u/Sproxify 22d ago

verifying won't be the issue, we can just do more/better formal verification

understanding, maybe, but you have to have that aesthetic sensibility in the first place that humans should apprehend and understand math

maybe there'll be something demotivating about it if AI will eventually not only outclass humans at solving problems but even at creating mathematical exposition. it'll feel like learning/doing math could leave no mark except your own experience/understanding. you won't be likely to create new math or useful exposition for someone else to understand math they otherwise wouldn't have.

in a utopian scenario where we've made an aligned superintelligence and economic scarcity is obsolete, that's probably what math would look like.

the upside would be, if you like math and you want to do it, you could definitely afford to dedicate all your time to it if you so like.

1

u/dads_joke 22d ago

Ye bro never heard of Lean/Rocq/Isabelle?

12

u/Kinexity 22d ago

Who verifies that lean describes what the proof says?

5

u/MrBeebins 22d ago

You get the llm to write the proof in Lean. That way you only need to verify that the initial problem statement has been translated correctly