>I think you should describe what counts as a theoretical breakthrough to you

It would be some new idea in proof theory that would produce significant reduction of required manual work in practical applications, making it easier for humans to work out the proofs and proof assistants help humans.

Linear logic, affine logic, etc. can provide incremental advantages, not breakthroughs.