Introduction - Justin Hart / PR #35705

Stream: new members

[Justin Hart]

Hi everyone! I'm Justin Hart, founder of Viridis LLC. I work at the intersection of formal verification, AI safety, and ecological modeling. I've been using Lean 4 to formalize results from my paper "The Intelligence Bound" (Hart 2025), which establishes information-theoretic bounds connecting entropy, ecological complexity, and computational intelligence.

I've just opened my first Mathlib PR — #35705 — which extracts two general-purpose lemmas from that formalization:

• ENNReal.div_eq_div_mul_div: division decomposition for extended non-negative reals
• • IndepFun.of_self: if Y is independent of itself under a probability measure, then X and Y are independent
    Looking forward to feedback and contributing more to the library!