From 21deacbe092fdc37254d5c60ede578d3d595fe35 Mon Sep 17 00:00:00 2001
From: lordwilson <theapexintelligence@gmail.com>
Date: Sat, 19 Sep 2026 09:59:03 -0500
Subject: [PATCH] Print huge natural-number literals in sub-quadratic time

`Nat.repr` (used by s!"{i}") converts a Nat to decimal one digit at a time,
each step a division of the whole number: quadratic in the digit count. A proof
term containing a literal with millions of digits stalls the exporter at 100% CPU
inside Nat.reprFast/toDigitsCore/gmpn_divrem_1 with no output.

natToDecStr splits by 10^(18*2^k) so GMP's sub-quadratic division does the work.
Output is identical to Nat.repr.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
---
 Export.lean | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/Export.lean b/Export.lean
index cda1993..aa6390d 100644
--- a/Export.lean
+++ b/Export.lean
@@ -4,6 +4,30 @@ import Std.Data.HashMap.Basic
 open Lean
 open Std (HashMap)
 
+/-! Decimal conversion of huge naturals. `Nat.repr` peels one digit at a time with a division of the
+whole number, which is quadratic and stalls for literals with millions of digits. This splits by
+10^(18*2^k) instead, so GMP's sub-quadratic division does the work. Output is identical to `Nat.repr`. -/
+partial def natToDecStrGo (pows : Array Nat) (k : Nat) (n : Nat) (pad : Bool) : String :=
+  if k == 0 then
+    let s := toString n
+    if pad then "".pushn '0' (18 - s.length) ++ s else s
+  else
+    let p := pows[k - 1]!
+    let q := n / p
+    let r := n % p
+    if !pad && q == 0 then natToDecStrGo pows (k - 1) r false
+    else natToDecStrGo pows (k - 1) q pad ++ natToDecStrGo pows (k - 1) r true
+
+def natToDecStr (n : Nat) : String :=
+  if n < 1000000000000000000 then toString n
+  else
+    let pows := Id.run do
+      let mut ps : Array Nat := #[1000000000000000000]
+      while ps.back! <= n do
+        ps := ps.push (ps.back! * ps.back!)
+      return ps
+    natToDecStrGo pows (pows.size - 1) n false
+
 def Lean.BinderInfo.toJson : BinderInfo → Json
   | .default => "default"
   | .implicit => "implicit"
@@ -166,7 +190,7 @@ partial def dumpExprAux (e : Expr) : M Nat := do
         ])
       ]
     | .bvar i => return .mkObj [("bvar", i)]
-    | .lit (.natVal i) => dumpNatDeps; return .mkObj [("natVal", s!"{i}")]
+    | .lit (.natVal i) => dumpNatDeps; return .mkObj [("natVal", natToDecStr i)]
     | .lit (.strVal s) => dumpStrDeps; return .mkObj [("strVal", s)]
     | .sort l => return .mkObj [("sort", ← dumpLevel l)]
     | .const n us => return .mkObj [