Comment by TripolitianFish
1 day ago
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.