News for hackers. Stuff that matters.
Re:Two-hundred-terabyte math proof is largest ever by clarus on Friday May 27, 2016 @12:59PM (#11787302)
In the community of the theorem prover Coq, a proof obtained by running a proven correct decision procedure is called a "proof by reflection".

There is also the "proof by certificate" approach. You generate a potentially large proof certificate by an unverified program. Then you run a proven correct (small) checker on the certificate to concude that the theorem is correct.

There are no comments on this comment yet.