It is entirely possible to use closed source black box programs to help develop proofs, all based on the fact that in a proof the existential quantifier does not require you to show you how you found the object, only prove that it satisfies the properties required. The program only needs to output the object, plus some "certificates" which can be used to check that the object satisfies the necessary proposition.
For example, consider integer factorization. Suppose you need to factorize a specific integer in your proof (for example a hard upper bound). Given a large integer, we don't care how some program factorizes it, in maths we only care about the factorization. The certificates are the factors, which can be multiplied to check that they are the factorization. Once we have the factorization the proof doesn't care how we got it.
Another example would be proving inequalities of polynomials in the reals. For this we can use sum of square decompositions, and semi-definite programming can give those decompositions. However, the proof doesn't need to know how we got the decomposition, only that we can certify that the given decomposition is indeed correct.
Now a lot of this changes if you use a different existential quantifier, like the constructivists. For these quantifiers more information might be necessary. Are we looking for an open source existential quantifier?
Slashdot Mirror
It is entirely possible to use closed source black box programs to help develop proofs, all based on the fact that in a proof the existential quantifier does not require you to show you how you found the object, only prove that it satisfies the properties required. The program only needs to output the object, plus some "certificates" which can be used to check that the object satisfies the necessary proposition.
For example, consider integer factorization. Suppose you need to factorize a specific integer in your proof (for example a hard upper bound). Given a large integer, we don't care how some program factorizes it, in maths we only care about the factorization. The certificates are the factors, which can be multiplied to check that they are the factorization. Once we have the factorization the proof doesn't care how we got it.
Another example would be proving inequalities of polynomials in the reals. For this we can use sum of square decompositions, and semi-definite programming can give those decompositions. However, the proof doesn't need to know how we got the decomposition, only that we can certify that the given decomposition is indeed correct.
Now a lot of this changes if you use a different existential quantifier, like the constructivists. For these quantifiers more information might be necessary. Are we looking for an open source existential quantifier?