# 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:** 5

<div class="post-metadata">

**Author:** ![matthias314](https://avatars.discourse-cdn.com/v4/letter/m/a88e4f/32.png) [@matthias314](https://discourse.julialang.org/u/matthias314)\
**Post date:** [October 25, 2026, 11:23pm UTC](https://discourse.julialang.org/t/formalizing-julia-in-lean-and-finding-400-bugs-in-base/140243/5 "2026-10-25T23:23:48Z")

</div>

Many abstract types in Julia don’t have precise interface definitions. (For instance, [it’s unclear](https://discourse.julialang.org/t/what-exactly-is-a-number/77331) what properties a `Number` has.) Without that, how can you prove anything about functions accepting such types?

---

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