Wikifunctions formalization
Giving Wikifunctions' executable functions the formal specification they lack — borrowed from Mathlib.
→ How these are verified — the deployed code, proved equal to its Mathlib spec.
WikiLean joins each Wikidata mathematics concept to two things: an Mathlib formalization, and a
Wikifunctions executable function (via the wikifunctionswiki sitelink on the shared
Wikidata item). The Wikidata QID is the join key. So for a function Wikifunctions can run
but cannot prove anything about, the matching Mathlib declaration becomes the formal
spec it was missing.
Of the 1,904 Wikifunctions currently linked to Wikidata, 25 fall in WikiLean's addressable set. For each we pin a computable oracle (the Mathlib decl or composed expression that produces the ground-truth value), grade whether that oracle is actually faithful to what the Wikifunction computes, and write a Lean spec stating its defining properties.
sorry, no axiom cheats. Every verdict is independently confirmed.
The 25 addressable functions
Grouped by verification tier. Each row links the Wikifunctions function (ZID), its Wikidata item (QID), and the Mathlib oracle pinned as ground truth. Hover a faithfulness chip for the reviewer's note.
composite-provable
— computable/decidable ℕ or ℤ oracle — conformance is provable in-kernel with decide.oracle-testable
— computable oracle as differential-test ground truth: exact ℚ/ℤ arithmetic, plus Float (IEEE-754 binary64) oracles for float64 functions.spec-only
— noncomputable real oracle only (e.g. arbitrary-precision Gamma) — specifies exact-ℝ behavior.composite-provable
15
computable/decidable ℕ or ℤ oracle — conformance is provable in-kernel with decide
oracle-testable
9
computable oracle as differential-test ground truth: exact ℚ/ℤ arithmetic, plus Float (IEEE-754 binary64) oracles for float64 functions
| Function | Wikidata | Mathlib oracle | Computability | Faithfulness |
|---|---|---|---|---|
| Z10862multiply numeric strings | Q40276 | HMul.hMul (or Nat.mul / Int.mul); for the decimal "full stop" format, Rat multiplication (· * ·) on ℚ | computable (ℕ/ℤ) | wrong target |
| Z12665exponentiation | Q33456 | (· ^ ·) on Float · ideal: Real.rpow | float64 | faithful |
| Z13341linear interpolation | Q2266329 | (1 - t)·a + t·b on Float · ideal: AffineMap.lineMap | float64 | faithful |
| Z21003natural logarithm | Q204037 | Float.log · ideal: Real.log | float64 | faithful |
| Z21005log base 10 | Q966582 | Float.log x / Float.log 10 · ideal: Real.logb 10 | float64 | faithful |
| Z21917complex conjugate (integer pair) | Q381040 | fun p : ℤ × ℤ => (p.1, -p.2) -- integer-pair conjugation; corresponds to starRingEnd ℂ via conj_re/conj_im (Complex.star z = ⟨z.re, -z.im⟩) | computable (ℕ/ℤ) | repr. mismatch |
| Z30840arithmetic mean | Q19033 | fun (l : List ℕ) => ((l.map (Nat.cast : ℕ → ℚ)).sum) / (l.length : ℚ) | computable (ℕ/ℤ) | wrong target |
| Z31173Euler characteristic | Q852973 | (fun (V E F : ℕ) => (V : ℤ) - (E : ℤ) + (F : ℤ)) -- elementary V - E + F; no dedicated Mathlib decl exists | computable (ℕ/ℤ) | wrong target |
| Z35278Shannon entropy | Q204570 | ∑ negMulLog over Float (bits) · ideal: Real.negMulLog | float64 | faithful |
spec-only
1
noncomputable real oracle only (e.g. arbitrary-precision Gamma) — specifies exact-ℝ behavior
| Function | Wikidata | Mathlib oracle | Computability | Faithfulness |
|---|---|---|---|---|
| Z16483gamma function | Q190573 | Real.Gamma | noncomputable ℝ | repr. mismatch |
What the cross-check found
Pinning a Mathlib oracle doubles as an audit of WikiLean's own AI-generated tags. As
originally mapped, only 9 of 25 were faithful for spec purposes: a recurring failure was a
tag pointing at a typeclass (the abstract algebraic structure, e.g. GCDMonoid,
AddCommMonoid) rather than the computable operation (Nat.gcd,
Nat.add). A typeclass can never serve as a value oracle. Each such case was corrected
to a concrete computable oracle, lifting the corpus to 14/25 faithful.
The remaining non-faithful rows are honest representation mismatches (right concept, wrong
encoding — e.g. a Gaussian-integer pair vs Mathlib's ℂ, or a
noncomputable Set.powerset vs the enumerable Finset.powerset), kept
visible rather than papered over.
Done: a verified composite-evaluator proof-of-concept — a small deep
embedding of the Wikifunctions composition language whose evaluator proves Z13701's
composite implementation equals(gcd(a, b), 1) equal to Mathlib's
Nat.Coprime (zero sorry; axioms = propext).
Next: generalize the evaluator to the remaining composite functions, and a
differential-testing harness that runs these oracles against the live Wikifunctions evaluator API.