[robinhouston]

Thanks for the pointer. I already had Avigad’s paper open on my computer, but I haven’t read it yet.

I take the point about the output – as opposed to the process – being “close to worthless”; though I suspect it’s only a matter of time before some result whose correctness ‘was never in doubt’ is found to be incorrect as a consequence of an attempt to formalize it.

[nextos]

I agree. The formalization is very impressive even if we consider it was done on a result that is already accepted as true and got a lot of help from humans to scaffold and build the structure.