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
Palli
October 29, 2026, 5:37pm
22
Maybe file an PR for this change? I timed it the same:
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.
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> @btime collect(StepRangeLen(0.9, nextfloat(0.9) - 0.9, 10))
29.148 ns (2 allocations: 144 bytes)
j-fu
October 30, 2026, 12:46pm
23
Just seen in the na-digest:
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
For a real Halloween fright… look at floor(x; sigdigits=1) near a power of 10!
Luckily it is fixable:
master ← MilesCranmerBot:bot/group-numbers-8
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)
