|
|
|
|
|
|
by drchewbacca
2460 days ago
|
|
|
It's not really like that. NN's are only used when searching for new proofs or steps which can be used to fill in details, the verification of a finished proof is done by a classical program by a series of substitutions which are very straightforward and spelled out in detail. Here is an example. https://arxiv.org/pdf/1608.02644.pdf |
|
|