The auto-formalization of mathematics versus law

Alan Yahya, writing on his blog, argues that while Anthropic's auto-formalization of Fermat's last theorem shows AI can structure vast literature, applying similar formal methods to law faces fundamental challenges, including ambiguity and contested facts. He proposes a shift toward AI formalization with machine verification, which could reduce legal matters to a small residue of critical points of contention.

The auto-formalization of mathematics versus law The auto-formalisation of Fermat’s last theorem vs the legal domain Alan Yahya https://www.linkedin.com/in/alan-yahya/ 3 min read I recently received a comment to this effect. "Isn't legal one of the things AI should in theory be very good at? Legalese is like code, in that every word is very strictly defined and there to do a specific job in the text." In practice, it's far from trivial to set up anything more formal than a loose taxonomy for legal matters. People have been trying for decades at least. And yet conceptually, the premise is there. What Anthropic demonstrated with its recent "auto-formalization" of Fermat’s last theorem, is that an AI swarm can quickly consume a vast quantity of literature, and represent it in a structured way. And clearly, that has the capability to be very useful to a human reader. But we’re still far from handing a judge 13.4 million lines of code to prove your client’s innocence, if indeed it should ever become possible. And yet: “AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered. “ \ 1\ reference-1 That this can be supported within mathematics, gives hope for downstream applications. Within the legal domain, the challenge is not to develop syntactically valid rules, but to ensure the legal fidelity of sourced text, which is difficult to quantify. First, let’s look at some general implementation details, which we might borrow to resolve problems in the legal domain. “Maintaining a directed acyclic graph DAG of theorem statements that agents used to decide what proofs they should attempt next. This was particularly helpful for mitigating memory degradation and allowing multiple agents to work in parallel.” \ 1\ reference-1 We released wrote about legal DAGs /blog/solving-legal-problems-with-dags . There’s nothing magical about DAGs, they’re just one measure to minimise the overhead cost of co-ordinating agents by preventing them from working on very similar areas. “Speeding up Lean compilation and minimizing resource consumption by separating theorem statements and proofs into different files, with the links between them maintained independently.” \ 1\ reference-1 This is essentially a point about information infrastructure: using deferred references /blog/see-inside-your-agents-to-fix-them an ongoing “wiki” rather than fused context, to reduce search work. Again, nothing groundbreaking here, just a logical separation of constraints. “Enabling search and reuse by maintaining a natural-language description of each theorem statement, resulting in a simpler proof path.” \ 1\ reference-1 As per above, deferred and optimised information retrieval becomes increasingly important as the problem grows in scale and complexity. So back to it, what can we actually achieve with a lean-style DSL for law? 1. Certainty that the conclusion follows from the encoded rules: yes. Once the rules and facts are formalised, inference can be checked deterministically. 2. Certainty that the law has been encoded correctly: sometimes. Unlike the explicit axioms in maths; legal texts may be ambiguous or contested. 3. Certainty that the encoded rule applies to the real-world facts: often no. Facts may be disputed, incomplete, or dependent on externalised concepts such as reasonableness, materiality, or intent. Our current system: Hand sources to LLM → AI produces a draft → lawyer checks everything The shift towards formalism: Hand sources to LLM → AI formalisation → machine verification → human-readable draft → lawyer reviews genuinely judgmental components which might happen to still be close to all of it . This gives us a picture of what legal AI may become: a machine that converts large matters into a small residue of critical points of contention. Whether that will be a further major paradigm shift remains to be seen. Ultimately, the advantage of auto-formalism will be to prevent verifiable factual mistakes, such as hallucinations and misfilings which are increasingly prevalent, but depend highly upon human intervention to mitigate . But there will always be nuance in law, as well as bias in AI models. That is why AI must continue to be used in a circumspect way, despite its undeniable utility for lawyers. References 1. Anthropic. Formalizing Fermat’s Last Theorem https://www.anthropic.com/news/formalizing-fermats-last-theorem . ↩ citation-1