Proof any student can multiply arbitrary numbers

Stream: lean4

[AbdulShabazz]

For entertainment purposes I gave OpenAI ChatGPT-4-oh v1.2025.196 the following scenario

Q: Posit a scenario wherein an engineering student is not allowed to matriculate through his/her/their chosen curriculum with a aid of a calculator without first demonstrating an ability to multiply arbitrary groups of numbers by hand (perhaps as an in-hand way for university to ensure their students still perform at high levels without the use of calculators!) What is a method which can be expressed as a formal LEAN 4 proof which demonstrates a student that performs on such a proof is capable of multiplying arbitrary groups of numbers ?

A: To express a method in Lean 4 that formally proves a student is capable of multiplying arbitrary groups of numbers, we must identify a general multiplication algorithm and construct a formal inductive proof demonstrating that the algorithm works correctly on arbitrary natural numbers (or integers, if signed multiplicands are needed).

The standard method of long multiplication — also known as "schoolbook multiplication" — is the most intuitive approach to represent formally and pedagogically relevant for university-level curricula.

---

Mathematical Concept

Let:

• a and b be arbitrary natural numbers

• a = aₙ * 10ⁿ + ... + a₁ * 10¹ + a₀

• b = bₘ * 10ᵐ + ... + b₁ * 10¹ + b₀

We want to show:

The multiplication a * b can be correctly computed by summing all partial products of digits of a and b, each scaled by the appropriate power of 10.

We formalize this by defining multiplication inductively over digits and/or positional decomposition.

---

Lean 4 Strategy

We define and prove the following in Lean 4:

1. A function digitMul for multiplying a number by a single-digit multiplier and returning the result.

2. A function longMul which recursively multiplies digit groups and accumulates them according to their decimal position.

3. A theorem longMul_correct: Proves that longMul a b = a * b for all natural numbers a and b.

---

Lean 4 Formalization

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Digits

open Nat
-- Multiply a natural number by a single digit (0 through 9)
def digitMul (a d : ℕ) : ℕ :=
  a * d
-- Recursively perform long multiplication using base-10 digits
def longMulAux (a : ℕ) (digitsB : List ℕ) (place : ℕ) : ℕ :=
  match digitsB with
  | []       => 0
  | d :: ds  => (digitMul a d) * (10 ^ place) + longMulAux a ds (place + 1)
-- Compute long multiplication of a and b
def longMul (a b : ℕ) : ℕ :=
  longMulAux a (Nat.digits 10 b) 0
-- Theorem: longMul computes the same value as standard multiplication
theorem longMul_correct (a b : ℕ) : longMul a b = a * b := by
  unfold longMul
  generalize hd : Nat.digits 10 b = digitsB
  induction digitsB generalizing a b with
  | nil =>
    simp [longMulAux]; rw [hd]; simp [Nat.digits_zero]
  | cons d ds ih =>
    simp [longMulAux]
    have : b = d * (10 ^ 0) + ofDigits 10 ds := by
      rw [←hd]
      apply digits_cons_decompose_base
      decide -- 10 ≥ 2
    rw [this, mul_add, mul_comm (a * d), ←mul_assoc, ←ih]
    sorry -- requires auxiliary lemmas about ofDigits, place value, etc.

---

Student Mastery Requirements (Informal Competency Outline)

To pass a calculator-free competency test grounded on this formal proof, a student must:

• Decompose any number b into its digits in base 10.

• Compute each digitMul a dᵢ.

• Apply the 10^i weight correctly to each partial product.

• Accumulate the results via addition.

Thus, the student demonstrates:

• Mastery of positional base-10 decomposition.

• Mastery of single-digit multiplication by arbitrary multi-digit numbers.

• Mastery of exponentiation by small integers.

• Mastery of addition of arbitrarily large intermediate results.

---

Lean Implications

Proving longMul_correct in Lean 4 assures us that any student capable of executing this decomposition and recomposition without a calculator is functionally equivalent to a student capable of computing arbitrary products.

Such a proof could be part of a formal verification track within an engineering curriculum where:

• Students not only perform the operations by hand,

• But also internalize the algorithmic structure by working through its formal proof.

This aligns with constructivist pedagogies and proof-as-program mindsets in advanced CS+Math education.

---

References

• Lean's Nat.digits and Nat.ofDigits implementation:
  https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Digits.html

• Church’s Thesis and Constructive Computability:
  https://plato.stanford.edu/entries/church-turing/

• Lean formalization tutorials:
  https://leanprover.github.io/functional_programming_in_lean/

I enjoy prompting ChatGPT with scenarios such as these :) I strongly recommend prompting ChatGPT on the impact of a formal proof of the Langlands Conjecture on the notion of computability; and using Lean 4 Metaprogramming along with goal-directed ontology generators to abstract common groups of assumptions into class/structure definitions, which can be refactored and generalized, as code and proofs, to create arbitrary synergetic structures...