> I don’t get upset. I just don’t know what that means.

metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:

1) the formal verifier (there are multiple re implementations)

2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)

3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons

A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.

Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.

If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").

Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?