formal-math

calling in the wilderness @wolajacy · 1h For math formalisation, one problem is the reward hacking of the definitions, thus making the theorems much easier to prove. And in principle, there no way to check the "validity" of definitions. Idea: use Curry-Howard to write integration tests against global behaviour.