If someone had a proof of the Collatz Conjecture, they might be advised to write a formal version of their proof in Lean or Coq, after which professional mathematicians would have to accept it.
Suppose this person wanted to keep the details of their formal proof a secret, though. Could they post a succinct certificate (a zero-knowledge proof) that confirms their proof works, without revealing the proof itself?
Generally speaking, is there an automatic system that converts any Lean proof (say) into an input for zkSNARK (say), generating such a certificate?
And would such a certificate be widely accepted?
Ah, while typing this post, I see that a 2024 paper attacks this problem. As they put it, “A zkPi proof is sufficiently short that Fermat could have written one in the margin of his notebook to convince the world, in zero knowledge, that he proved his famous last theorem.” 
PS. Cryptographer William Friedman did something spiritually similar when he put his one-sentence theory about the Voynich Manuscript into a sealed envelope, then published an anagram of it in a 1959 paper, effectively time-stamping the idea.