[lioeters]

There's a parallel with open source software (FOSS), that you don't really control the software if you don't have the source code.

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.