# 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:** 1\
**Showing post:** 15

<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:** [October 27, 2026, 12:15am UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/15 "2026-10-27T00:15:58Z")

</div>

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

```julia-auto
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](https://github.com/JuliaLang/julia/issues/64272))

Also, `tanh(::Float32)` appears to be [locally non-monotonic](https://github.com/JuliaLang/julia/issues/64225) at an ordinary Float32 value:

```julia-auto
julia> x = 0.49214557f0;

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

```

---

_[View the full topic](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243)._