Japanese Multiplication Proof
lattice multiplication, machine-checked in ACL2s
Proves the lattice multiplication trick is not a coincidence: the theorem prover confirms it equals standard multiplication for every pair of numbers and every base, not just the examples you can draw.
Each digit becomes a bundle of parallel lines. Where the bundles cross, the intersections cluster along diagonals, and each diagonal is one column of the answer. Step through with Next, or focus the board and use the arrow keys.
This is the procedure ACL2s machine-checked: jmult-equiv proves the diagonalize and flatten pipeline equals ordinary multiplication for every pair of numbers and every base, not just the ones drawn here.
Draw the lines. 21 is drawn as 2 line bundles crossing 13 as 2 bundles.
Step through the lattice method the proof formalizes: line bundles, diagonal intersection counts, carries, and the final product.
The source for this course project is kept private. Request access through the contact form and I will gladly share the code and walk through it.
Request accessA CS2800 (Logic and Computation) final project, built by a team of four, that takes the well-known schoolyard trick of multiplying by drawing crossing lines and counting their intersections, and proves it correct once and for all in the ACL2s theorem prover. Numbers are modeled in reverse-digitized form as lists of natural numbers (the lon and lolon algebraic data types), and the lattice procedure is reconstructed as pure recursive functions: scale distributes one digit across the other operand, diagonalize collects the intersection counts into diagonals, flattenlolon sums each diagonal into a carry-free column total, and list-to-num reassembles those columns into a number in a given base. The headline theorem, jmult-equiv, states that for any two digit-lists and any base, this whole pipeline equals normal-mult, the ordinary product. ACL2s discharges it by first proving an intermediate distribute-mult equals normal multiplication, then proving the lattice pipeline equals distribute-mult, with a chain of supporting lemmas about how list-to-num distributes over scaling, appending, and flattening. Where the prover could not find the induction on its own, the team supplied the key subgoals by hand. The result is a parameterized, base-agnostic correctness guarantee, not a spot check on a few examples.
- ACL2s
- Common Lisp
- Formal methods
- Theorem proving
- Inductive proofs
- Verified functions
- 9 (definec)
- Theorems proven
- 28 (defthm)
- Data types
- 2 (lon, lolon)
- Result
- lattice = standard, any base
What I'd improve
The proof leans on several subgoals supplied by hand because the prover would not find the right induction unaided, and a handful of supporting lemmas are stated as accepted axioms rather than themselves proven from first principles. With more time I would tighten those, removing the hand-fed subgoals in favor of better induction hints and discharging every lemma so the trusted base is as small as possible.