IMO an interesting project in this space is: mm0 / MetaMath Zero - Closing the loop in proof verification down to verifying the machine code of the verifier. Go

IMO an interesting project in this space is: mm0 / MetaMath Zero - Closing the loop in proof verification down to verifying the machine code of the verifier. Goes from first-order logic to peano arithmetic to a model of x86 to a model of the verifier written in x86. Interestingly, it demonstrates that verification of a compact proof can be performed in linear time (!) if the proof is structured correctly. -- https://github.com/digama0/mm0 https://github.com/digama0/mm0 The fact that proof checking can take linear time (though not proof-finding), and the fact that it incorporates so many 'layers' has emboldened my opinion that such a thing as I described above is possible and has enormous potential.