@TimothyChow So you involve a reverse engineering activity here. Thought about this. I would like to forbid this by requiring my machine (this human) not to "cheat" by learning from other machines. He has access only to existing books and papers, as well as existing algorithms described in human language, but not existing implementations of the algorithms. By the way, I don't think my idea is perfect, not even well-defined. But I enjoy any discussion / opposition that could make it better, ultimately towards a well-defined standard for computer involvement in maths.

@TimothyChow The "unless you make the effort" part is way weaker than my "purely logic possibility with infinite time". As in "science is fausifiable", physics is science because there is a hypothetical scenario that makes it false, which does not mean it's actually false. Moreover, I'm making the statement with an ideal machine (human with infinite time and always enough knowledge). All algorithm should run with this machine, so compiler, os, hardware are not in the equation.

@TimothyChow my requirements do not extend to compiler, OS or hardware, but let me explain. Fot a proof to be acceptable, there should be a purely logic possibility that any human being, given infinitely much time and enough knowledge, could work out every step of the algorithm. This is possible once the algorithm and the necessary knowledge is accessible. OS etc. doesn't matter here. But if aliens come with a machine that is said to do multiplication with a more advanced method that humans do not have access/understand, then mathematicians should not use this machine for any proof.

@TimothyChow Actually, I think you do ... In the scenario of a "computer added proof", where the plan involves billions of multiplications (so that we have to use computer), the best case would be that each multiplication is verifiable by author, the second best case would be that the implementation and algorithm of multiplication is accessible and verifiable by author, although the author does not need to really do these. This is my threshold. So the author should at least write their own code, or use and cite openly accessible code.

I use "computer aided proof" for the case where a human set up a plan and computers do the work. This can then be verified by checking the plan and the implementation. I use "computer calculation" for the case where a human use a software, whose algorithm he does not read / not completely understand, just for an output.

I think we need to distinguish "computer aided proof" (your case) and "computer calculation" (OP's case). I support the former and regard it as a solid math proof, but I strongly oppose the latter as proof in any sense.

@DimaPasechnik I was a heavy user of Sage until recently, when I begin to work a lot with elliptic functions. I tried many OSS (pari/gp, mpmath, scipy etc.) and finally obtain a Mathematica license from my university. Although Mathematica also fails me, I must say that industrial softwares are very powerful in some aspects that OSS cannot compete with. This is very different from Elsevier vs OA. But on the other hand, I never publish anything that the reader would need Mathematica to verify, i.e. I never put my readers behind any paywall.

@IosifPinelis In PO's case (very complicated function and a numerical output), I strongly doubt that Maximize[] has called NMaximize[], but PO could only become aware of this possibility if he is an expert, or has read the manual very carefully (does MMA throw a warning?). That aside, I support "computer aided proof", where humans make the plan and computers do the work. But I oppose "computer calculation" as proof, where humans give up understanding and ask software written by others to output a number. In PO's case, I would only accept if he completely understands Maximize[]'s algorithm.

@IosifPinelis Sure, both humans and computers make mistakes. Human mistakes arise from insufficient (but still deep) understanding, and can be checked then corrected by improved understanding. But if a result is obtained solely by computers, it often means that humans hardly have any understanding. If there is any mistake, it can only be discovered and corrected once humans begin to have some understanding. It is either a mathematical proof, or a human certifiable program. We do mathematics for humans to understand, not to generate numbers for humans to believe.