There seems to be a kind of Heisenberg uncertainty relation type constraint: the tradeoff between intelligibility and certainty. Writing a proof with a dependent type theory based proof assistant is much like the entropy increasing process of encryption. The encryption process is clear, the person who is proving lemmas and theorems in the proof assistant understands the proof and understands what they are doing - which is kind of like a game. But the result is ultimately incomprehensible and impossible to decrypt without the knowledge of the original proof or without attempting to generate the formal proof oneself by playing the game.
Thus we are lead to choose somewhere between the extremes of intelligibility and uncertainty or certainty and unintelligibility.
I believe we need a whole new approach to proof-assistant and indeed to formal axiomatic-deductive system which takes into account the multi-leveled and high-level forms of reasoning and expression in natural language based mathematics.
No comments:
Post a Comment