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

General Usage
15

Some of these new ones are wild. Not sure I would ever notice without formal verification:

julia> collect(LinRange(0.1, 0.1, 5))
5-element Vector{Float64}:
 0.1
 0.1
 0.1
 0.1
 0.1

julia> collect(LinRange(0.1, 0.1, 6))
6-element Vector{Float64}:
 0.1
 0.10000000000000002
 0.1
 0.1
 0.1
 0.1


julia> collect(LinRange(0.1, 0.1, 7))
7-element Vector{Float64}:
 0.1
 0.1
 0.1
 0.1
 0.1
 0.1
 0.1

(Issue: LinRange(0.1, 0.1, 6) is not constant · Issue #64272 · JuliaLang/julia · GitHub)

Also, tanh(::Float32) appears to be locally non-monotonic at an ordinary Float32 value:

julia> x = 0.49214557f0;

julia> tanh(x) > tanh(nextfloat(x))
true