|
|
|
|
|
|
by c7b
7 days ago
|
|
|
The endangered art form of human mathematics is one thing. Another thing is that there seems to be little concern for whether a theorem was created using a documented open-weights model or some unknown model in a web chat. If you want to make the case that the journey of creating the proof is part of doing mathematics, then you should also document that path and make it reproducible, as science should always be. There were some examples of mathematicians publishing their AI proofs like that in the last days, but by far not all. |
|
|
Being given only the generated proof (or disproof) is like having the binary artifact as an executable. Sure you can use it to solve or build further on top of it, but without the source code - the understanding of the steps to build the binary - you can't build it yourself, and you don't actually own it. If you want to adjust or extend something in the proof, you have to go back to a third party to implement it and generate another artifact for you.
We need a Stallman for mathematics with uncompromising integrity, to shout from the rooftops for a "free and open-source math movement" (FOSM). Even if the biggest AI companies go bankrupt, we still need to be able to bootstrap all the math from the source code.