> People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.

I don’t get upset. I just don’t know what that means. What would that look like in practice?

Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”

How would you write that in mathematical formalization?

And then how would you make a metamath verifier judge if Robert J. Rippee committed it on January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“

How would something like that look like under your proposed system?