# Formalizing Julia in Lean (and finding 400+ bugs in Base)

**URL:** <https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243>\
**Category:** General Usage\
**Created:** [October 25, 2026, 7:07pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243 "2026-10-25T19:07:11Z")\
**Posts on this page:** 5\
**Page:** 2

<div class="post-metadata">

**Author:** ![ParadaCarleton](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/paradacarleton/32/20005_2.png) [@ParadaCarleton](https://discourse.julialang.org/u/ParadaCarleton)\
**Post date:** [October 27, 2026, 7:29pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/21 "2026-10-27T19:29:16Z")

</div>

This is amazing, and thank you so much for all your hard work! How reusable is this code—is there a package or something for finding errors in Julia with Lean? That’d be awesome to see 🙂

---

<div class="post-metadata">

**Author:** ![Palli](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/palli/32/3380_2.png) [@Palli](https://discourse.julialang.org/u/Palli)\
**Post date:** [October 29, 2026, 5:37pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/22 "2026-10-29T17:37:10Z")

</div>

> [@MilesCranmer](#):
>
> If you mend Julia’s `lerpi` to do the same .. (which is fewer FLOPs, too!) then the same range steps up once

Maybe file an PR for this change? I timed it the same:

```julia-auto
julia> @btime collect(LinRange(0.9, nextfloat(0.9), 10))
  27.814 ns (2 allocations: 144 bytes)

```

[Before and after 2 allocations, both 144 bytes, but should either allocate? Might be about global scope.] Maybe slightly faster, or just noise, at least not slower.

> [@tim.holy](#):
>
> Floating-point exactness is the domain of `StepRangeLen`

What do you mean? We should compete with `np.linspace` with `LinRange` (not with `StepRangeLen`?!). `StepRangeLen` gives a different result and also with, if you meanst something like that:

```julia-auto
julia> @btime collect(StepRangeLen(0.9, nextfloat(0.9) - 0.9, 10))
  29.148 ns (2 allocations: 144 bytes)

```

---

<div class="post-metadata">

**Author:** ![j-fu](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/j-fu/32/11373_2.png) [@j-fu](https://discourse.julialang.org/u/j-fu)\
**Post date:** [October 30, 2026, 12:46pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/23 "2026-10-30T12:46:11Z")

</div>

Just seen in the na-digest:

```julia-auto
From: Diana Halikias diana.halikias@nyu.edu
Date: October 27, 2026
Subject: Lean + Numerical linear algebra working group

We are running a biweekly working group over Zoom to discuss integrating
Lean and NLA research. Topics include an NLA Lean library, incorporating Lean
in combination with AI into our research workflows, proof formalization
standards for the research community, and theoretical underpinnings of Lean.
Our next meeting is Tuesday, Nov 10 at 9:30am eastern time. If you are
interested in joining the email list, please contact diana.halikias@nyu.edu. You
can also view the slides from our first meeting on the website:
dihalikias.github.io/lean-nla.html

Diana Halikias and Haim Avron

```

---

<div class="post-metadata">

**Author:** ![MilesCranmer](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/milescranmer/32/21070_2.png) [@MilesCranmer](https://discourse.julialang.org/u/MilesCranmer)\
**Post date:** [November 3, 2026, 8:10pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/24 "2026-11-03T20:10:40Z")

</div>

For a real Halloween fright… look at `floor(x; sigdigits=1)` near a power of 10! 🫣

 ![image](https://global.discourse-cdn.com/julialang/original/3X/3/e/3e5cd7fb6c83b1b0bbd7e41c5c8c2ba801f45383.png)

Luckily it is fixable:

> <https://github.com/JuliaLang/julia/pull/64624>
>
> Fixes #64186, fixes #45880, fixes #64121, fixes #64125, fixes #64177.
> 
> Seven sma…ll, independent bug fixes in rounding, integer arithmetic and digit extraction, found while formalizing Base in Lean. Each is a separate commit with its own test, so they can be reviewed or dropped one at a time.
> 
> \### 1. \`floor\` with \`sigdigits\` returns zero just below a power of ten
> 
> \`\`\`julia
> julia\> floor(prevfloat(1000.0); sigdigits=1)
> 0.0 # should be 900.0
> 
> julia\> trunc(prevfloat(1000.0); sigdigits=1)
> 0.0 # should be 900.0
> 
> julia\> floor(prevfloat(100.0); sigdigits=1)
> 0.0 # should be 90.0
> 
> julia\> floor(Float16(99.94); sigdigits=1)
> Float16(0.0) # should be Float16(90.0)
> 
> julia\> floor(999.9999f0; sigdigits=1)
> 0.0f0 # should be 900.0f0
> \`\`\`
> 
> \`base/floatfuncs.jl:133\` estimates the leading decimal position with \`log10\`, which can round up to an integer and select a rounding step ten times too large. The fix corrects estimates near an integer with an exact comparison to the power of ten, using directed rounding at the input precision for \`BigFloat\`. This complements #63105, which makes the rounding to that position exact: with both, \`floor(prevfloat(0.1); sigdigits=1)\` is \`0.09\` and \`round(prevfloat(1000.0); sigdigits=16)\` is \`999.9999999999999\`.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/floatfuncs-sigdigits-hidigit.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/FloatFuncs/Refuted.lean#L44)
> 
> \### 2. \`nextpow\` returns wrapped results when the next power does not fit
> 
> \`\`\`julia
> julia\> nextpow(2, Int8(65))
> \-128 # should be OverflowError
> 
> julia\> nextpow(2, typemax(UInt8))
> 0x00 # should be OverflowError
> 
> julia\> nextpow(Int8(7), Int8(50))
> 87 # should be OverflowError
> 
> julia\> nextpow(Int8(7), Int8(88))
> 97 # should be OverflowError
> \`\`\`
> 
> \`base/intfuncs.jl:650\` returns the power-of-two fast-path result without checking overflow, and its general path can accept a wrapped integer power that happens to increase. The fix checks the fast-path result against the input and uses \`checked\_pow\` for integer bases in the general path.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/intarith-powers-nextpow-overflow.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/intfuncs.lean#L1285)
> 
> \### 3. \`checked\_pow\` treats the largest unsigned integer as \`-1\`
> 
> \`\`\`julia
> julia\> Base.Checked.checked\_pow(UInt8(255), Int8(-1))
> 0xff # should be DomainError
> 
> julia\> Base.Checked.checked\_pow(UInt8(255), -2)
> 0x01 # should be DomainError
> \`\`\`
> 
> \`base/intfuncs.jl:421\` recognizes the \`-1\` unit with \`isone(-x)\`, which also succeeds when unsigned negation wraps the largest value to one. The fix excludes unsigned values and complex values with unsigned components from that unit check in the shared \`power\_by\_squaring\` implementation.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/intarith-checked-negative-pow.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/checked.lean#L1459)
> 
> \### 4. \`digits\` rejects a valid \`typemin\` negative base
> 
> \`\`\`julia
> julia\> digits(5; base=typemin(Int))
> ERROR: DomainError with -9223372036854775808: # should be \[5\]
> base must be ≥ 2 or ≤ -2
> \`\`\`
> 
> \`base/intfuncs.jl:1250\` validates the base with \`abs(base)\`, which wraps for \`typemin\`, and the negative-base digit loops and unsigned digit-count path also negate that base in its original type. The fix uses the existing overflow-safe \`uabs\` helper for validation and negative-base division in both \`digits!\` and \`ndigits0znb\`.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/parseprint-digits-typemin-base.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/Proofs/base/intfuncs.lean#L1316)
> 
> \### 5. \`digits\` wraps negative \`BigInt\` digits into unsigned values
> 
> \`\`\`julia
> julia\> digits(UInt8, big(-7))
> 1-element Vector{UInt8}:
> 0xf9 # should be InexactError
> 
> julia\> digits(Integer, big(-7))
> 1-element Vector{Integer}:
> 0xf9 # should be -7
> \`\`\`
> 
> \`base/gmp.jl:787\` writes positive digit magnitudes through its fast paths and then negates the stored values, so unsigned digits wrap and abstract integer arrays can retain unsigned elements. The fix sends negative inputs through the generic implementation unless the destination element type is signed.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignums-digits-unsigned-negative.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNums/Int.lean#L321)
> 
> \### 6. \`digits!\` into a short view throws for a \`BigInt\` and a power-of-two base
> 
> \`\`\`julia
> julia\> digits!(view(zeros(Int, 10), 1:3), big(2)^62 + 5; base=128)
> ERROR: MethodError: no method matching resize!(::SubArray{Int64, 1, Vector{Int64}, Tuple{UnitRange{Int64}}, true}, ::Int64) # should be \[5, 0, 0\]
> \`\`\`
> 
> \`base/gmp.jl:803\` accepts unit-stride views in the \`mpz\_export\` fast path, whose destination may need resizing even though views do not support \`resize!\`. The fix restricts that fast path to \`Vector\` and lets other destinations use the existing generic digit loop.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignums-digits-view-pow2-base.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNums/Int.lean#L334)
> 
> \### 7. Scoped \`setprecision\` accepts invalid precision and base values
> 
> \`\`\`julia
> julia\> setprecision(() -\> 7, BigFloat, 0)
> 7 # should be DomainError
> 
> julia\> setprecision(() -\> 7, BigFloat, 10; base=1)
> 7 # should be DomainError
> \`\`\`
> 
> \`base/mpfr.jl:1221\` installs the converted precision in a scoped value without the validation performed by the global setter. The fix checks that the base is at least two and the precision is positive before running the callback.
> 
> \[Bug report\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/bugs/bignumscov-scoped-setprecision-validation.yaml), \[Lean proof\](https://github.com/MilesCranmer/julia-in-lean/blob/8c53f61/julia-base/JuliaLean/BigNumsCov/Mpfr.lean#L533)

---

<div class="post-metadata">

**Author:** ![langestefan](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/langestefan/32/207923_2.png) [@langestefan](https://discourse.julialang.org/u/langestefan)\
**Post date:** [November 3, 2026, 8:33pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/25 "2026-11-03T20:33:39Z")

</div>

![image](https://global.discourse-cdn.com/julialang/original/3X/5/b/5bcafdabeeccb5f404c54509fce7fe3975f2c74d.png)

[Previous page](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243.md?page=1)