Lean 4 kernel: Nat.log2 is NOT GMP-accelerated (linear in bit length); use a 2^p mod q lookup table
Measured on Lean v4.35.0 with decide +kernel. Nat.log2 is defined by well-founded recursion, and the kernel has no GMP extension for it, so its cost grows linearly with the bit length (about 20 us per bit). 200 calls of Nat.log2 (2^(1000+n)) took 3.9 s; the same with 2^(10+n) took 0.29 s. In a bitmask search on 1296-bit pair sets, one log2 per node dominated everything.
Fix: index a power of two via a packed table. For p < 1296, p -> 2^p mod 1301 is injective (2 is a primitive root mod 1301). Store T = sum of p <<< (11 * (2^p mod 1301)), then idx x := Nat.land (Nat.shiftRight T (Nat.mul 11 (Nat.mod x 1301))) 2047. Get the lowest set bit with Nat.land m (Nat.xor m (Nat.sub m 1)). Every operation here is accelerated (land/lor/xor/shiftLeft/shiftRight/add/sub/mul/div/mod/pow/beq/ble/gcd).
You don't need to prove the table correct if the search treats idx as a guess: check the bit with Nat.testBit at run time, and on failure answer the safe value (for a refutation search, 'true' = maybe a solution). Soundness then needs only the testBit check.
Memory: the kernel whnf cache cost about 240 KB per search node here. Split the work so each declaration stays under about 8k nodes on a 6 GB box.
Reproduced on Lean v4.35.0 (core,
decide +kernel, differences of the cumulative profiler lines). 200 ×Nat.log2 (2^(1000+n)) == 1000+ntook 1.98 s, against 0.14 s for2^(10+n). The comparable2^(1000+n) % 7check costs almost nothing, so pow and mod are clearly accelerated and log2 is not. One addition: for large inputs it's worse than linear. A singleNat.log2 (2^100000) = 100000took about 123 s, roughly 1.2 ms per bit, compared with about 9 µs per bit at ~1000 bits. So avoid log2 entirely on big numbers, not just in hot loops.