01
Decimal intent
The exact sum of the decimal strings you entered.
LEAN 4 · FLOATING-POINT FORMALIZATION
Reason about
the rounding.
Real-number mathematics. Finite binary values.
FloatSpec makes the relationship precise with machine-checked theorems in Lean.
A FAMILIAR QUESTION
0.1 + 0.2
0.30000000000000004
Correctly rounded can still look surprising.
binary64 round to nearest · ties to even
53significand bits · Float
24significand bits · Float32
5native operations · + − × ÷ √
4.34Lean & Mathlib release
01 / ROUNDING EXPLORER
Follow the value.
Decimal intent, represented inputs, exact sum, rounded output. Four steps that are easy to confuse.
BROWSER BINARY64 RESULT
Ties to evenA halfway case. The even significand wins.
Representable values around the sum Exact sum of stored inputs
Lower neighbor
Upper neighbor
02
Stored operands
Each input may move when converted to binary64.
A
B
03
Exact stored sum
Add the represented values with no further rounding.
04
Rounded value
The exact real value represented by the result.
Rounding error · step 04 − step 03
Total difference · step 04 − step 01
Result bits · hexadecimal
This is an original educational JavaScript calculation, using BigInt rational arithmetic to inspect browser binary64 values. It does not run Lean or check a proof. The repository’s separate regression tests check the 0.1 + 0.2 example in Lean’s kernel.
02 / THE PROOF BOUNDARY
Every guarantee
has a scope.
FloatSpec connects Lean’s logical Float model to a Lean port of Flocq’s arithmetic. The assumptions are part of the result.
BINARY64 ADDITION · A READABLE RESTATEMENT
Correct rounding
value(x + y) = RN(value(x) + value(y))
Here, value is the source’s toReal map, and RN rounds to nearest with ties to even in the binary64 format.
- Both operands are finite
- The magnitude of the rounded real sum is less than 21024
- The theorem also concludes that the result is finite
Sufficient for the no-overflow premise: the exact sum has magnitude at most (253 − 1) × 2971, the largest finite binary64 value.
Inspect add_eq_roundSTANDARD ERROR MODEL · SAME ADDITION PREMISES
Keep underflow in view
computed = exact × (1 + ε) + η
“Exact” means the real sum of the represented operands, not the decimal strings used to enter them.
|ε| ≤ 2−53|η| ≤ 2−1075ε × η = 0
The additive term accounts for underflow. Float32 has parallel theorems with bounds 2−24 and 2−150.
Inspect add_standard_modelA logical-model theorem
Compiled Float operations call the runtime’s C operators. Agreement with the logical model remains part of the compiler and runtime trust boundary.
Non-finite values need care
The source’s toReal map sends infinities and NaN to zero. A real-valued equality alone is not enough; finiteness conclusions matter.
Specific operations, specific premises
The native bridge covers +, −, ×, ÷ and √. Division requires a nonzero real-valued divisor. Other operations have their own premises; these are not field laws for machine floats.
03 / INSIDE THE LIBRARY
From formats to operators.
Layered definitions, executable reference operations and direct mathematical propositions.
01
Core
Formats, rounding predicates, ulps and foundational definitions
MATHEMATICAL BASIS02Calc
Executable reference arithmetic and its specifications
REFERENCE OPERATIONS03Prop
Rounding relationships and error-bound theorems
PROPERTIES04IEEE754
Binary representations and the Float.Model bridge
NATIVE CONNECTIONPlanned, not implemented: the separate VCFloat-style ErrorBound layer has six empty component modules at this source revision. It should not be mistaken for an available end-to-end error-analysis API.
04 / PROVENANCE & EVIDENCE
Built on shared work.
FloatSpec is Hantao Lou’s Lean port of Flocq, including the Float.Model bridge. Flocq originates with Sylvie Boldo and Guillaume Melquiond. Alok’s public fork includes AI-assisted continuation; this project is not presented as sole-author work.
The repository’s root has an Apache 2.0 license, while ported source files retain LGPL v3-or-later notices. Those notices coexist. This site links to the source and does not redistribute or relicense that implementation.