Comment by nickysielicki | Hacker News Reader

Comment by nickysielicki | Hacker News Reader

Parent Full thread

1. why can’t the so called “real mathematicians” (as if mathematics does not belong to all of us) write the lean theorems by hand and then we let the machine fill the rest in? They are very upset that they can no longer contribute to frontier mathematics. This would let them contribute.

2. Why shouldn’t math progress happen in the open, commit by commit? Why is it so horrible if a proof is 95% of the way there but we later find that it needs to be refined? Mathematics previously was optimizing for an antiquated publishing and distribution scheme. There is no need for the first print to be correct. We have the internet now. We can and should publish incomplete results and correct things on the fly. Maybe mathematicians would have solved some of these problems years ago if they didn’t hide incomplete almost solutions in their filing cabinet because it wasn’t yet ready to be published.

You don’t hate the pageantry of mathematics and academics enough.

About your second point.

I bet you enjoy when a peer asks you to find the issues in a fully AI generated PR that’s 95% of the way there.

...and the peer also insists that's 100% finished. :'(

You’re right. But to quote Don Draper, “That’s what the money’s for!”

What are you even saying. Mathematics largely happens “commit by commit” as insufferable as that is a way of saying it, via conferences and meetings and prepublications. You’re attributing some bizarre to morality how mathematicians operate. You’re just upset people aren’t playing at your playground enough to your liking.

Also “real mathematicians” aren’t the people who “math belongs to”, you’re a mathematician if you do math, that’s it.

I mean git commit by git commit. Which is how it looks when you use the right tool, eg: lean4

I'm sorry if I've misinterpreted you, but:

1. In OpenAI's case, they dumped 1.8 GiB of Lean proofs on the world. I don't think they've done anything ethically wrong by doing that, but it's the exact opposite of "commit by commit". In fact, I'd say human mathematics has been much closer to "commit by commit", usually using smaller results as stepping stones.

2. You can have "commit by commit" without formal provers like Lean. Just keep your text in a Git repo.

I mean 95% of a proof is not a proof, and the fact that we got 95% of the way there isn't necessarily an indication that we'll ever get there. There's also a big difference between publishing a mostly-done proof as such and publishing a proof as complete only to retract later.

There's a lot to hate about the academic world, but the solution isn't spewing out terabytes of crappy half-baked results.

Reply on news.ycombinator.com