In the 17th Century, the philosopher, mathematician, and lawyer Gottlfried Leibniz envisioned the creation of a *characteristica universalis* and *calculus ratiocinator* that would enable reasoning in law and morals as systematically as in geometry and analysis. His goal was to resolve legal disputes with the precision and clarity with which accountants settle financial discrepancies. “To take pen in hand, sit down at the abacus and, having called in a friend if they want, say to each other: Let us calculate!” 

 We are now, for the first time in history, positioned to realize Leibniz's dream of automating legal reasoning. The crucial step in this process, I will argue, is the alignment of sophisticated computer science techniques with appropriate types of legal problems. Automating code-based legal reasoning, which relies on explicit statutes and regulations, differs fundamentally from automating case-based reasoning, which depends on precedents and interpretations. I will explore how formal methods and Large Language Models (LLMs) can be utilized to achieve what Leibniz envisioned three centuries ago, effectively transforming the landscape of legal reasoning through the power of modern computational technology.