Numerical analysis
The Lean Pool projects whose card's first MSC2020 code is in class 65, Numerical analysis: 3 articles, one per card.
TheoremCertified Runge-Kutta Order Conditions#
Certifies Runge-Kutta order conditions over planar rooted trees, including RK4 order four, Dormand-Prince order five, and Gauss-Legendre order six.
Quoted from the card LeanPool/projects/runge-kutta-order-conditions.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 8 main results, each with its informal statement quoted from the card. The scan finds 8 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
RungeKuttaOrderConditions.Butcher.satisfiesOrderConditions_iff(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 453: “Reduces order-p Runge-Kutta conditions to a finite catalogue check over rooted trees.”RungeKuttaOrderConditions.Butcher.rk4_order4(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 462: “Certifies that classical RK4 satisfies all planar rooted-tree order conditions through order four.”RungeKuttaOrderConditions.Butcher.rk4_not_ord5(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 342: “Shows that RK4 fails a fifth-order condition, pinning its order exactly.”RungeKuttaOrderConditions.Butcher.orderCond_node_perm(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 531: “Proves order conditions are invariant under permutations of a node's children.”RungeKuttaOrderConditions.Butcher.dp_order5(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 625: “Certifies the Dormand-Prince RK45 fifth-order tableau through order five.”RungeKuttaOrderConditions.Butcher.gauss_order4(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 777: “Certifies the Gauss-Legendre three-stage tableau through order four over Q(sqrt(15)).”RungeKuttaOrderConditions.Butcher.gauss_order6(theorem), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 839: “Certifies the denominator-cleared (360-scaled) integer Z(sqrt(15)) Gauss-Legendre tableau through order six, the scaled certificate feeding the homogeneity bridge.”RungeKuttaOrderConditions.Butcher.gauss_order6_rat(theorem; a main declaration), declared in LeanPool/RungeKuttaOrderConditions/ButcherOrder.lean, line 1003: “Certifies the Gauss-Legendre s=3 tableau through order six over Q(sqrt(15)), via the formalized homogeneity bridge from the 360-scaled integer certificate.”
Project
- Authors: Carles Marín.
- Source: What Order a Method Knows by Carles Marín, doi:10.5281/zenodo.20787666.
- Project repository: karlesmarin/runge-kutta-order-conditions-lean.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 65L06, 65L05, 05C05.
- In Lean Pool: LeanPool/RungeKuttaOrderConditions, from the card LeanPool/projects/runge-kutta-order-conditions.yaml.
Sources
InductiveFlean: Floating-Point Numbers in Lean#
Formalizes a configurable model of floating-point numbers in Lean 4, including normal and subnormal representations, conversions between rationals and floats, round-trip correctness, and rounding error bounds.
Quoted from the card LeanPool/projects/flean.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Flean.Float(inductive; a main declaration), declared in LeanPool/Flean/Basic.lean, line 47: “Defines the floating-point number type parameterized by a precision and exponent configuration, with normal, subnormal, infinite, and NaN cases.”toFloat(def; a main declaration), declared in LeanPool/Flean/Basic.lean, line 59: “Rounds a rational number to the nearest representable floating-point value under a given rounding mode.”toRat(def; a main declaration), declared in LeanPool/Flean/Basic.lean, line 90: “Interprets a floating-point value as the exact rational number it represents.”to_float_to_rat(lemma; a main declaration), declared in LeanPool/Flean/Basic.lean, line 233: “Proves the round-trip identity that converting a finite nonzero float to a rational and back recovers the original float.”roundf_close(lemma; a main declaration), declared in LeanPool/Flean/Rounding.lean, line 541: “Bounds the distance between a rational and its rounded floating-point representation.”
Project
- Authors: Joseph McKinsey.
- Source: doi:10.1109/IEEESTD.2019.8766229.
- Project repository: josephmckinsey/flean.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 65G50, 65G30, 68V20.
- In Lean Pool: LeanPool/Flean, from the card LeanPool/projects/flean.yaml.
Sources
StructureVerified interval-Cauchy real arithmetic#
Represents real numbers as Cauchy sequences of nested rational intervals quotiented into a field, with executable interval ring arithmetic, proven-convergent rational bounds for sqrt, exp, and pi, and an IsComputable typeclass that packages such approximations to drive classical (noncomputable) comparison instances, after O'Connor's certified exact real computation.
Quoted from the card LeanPool/projects/computablereal.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 5 main results, each with its informal statement quoted from the card. The scan finds 5 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ComputableℝSeq(structure; a main declaration), declared in LeanPool/ComputableReal/ComputableRSeq.lean, line 132: “A sequence of converging rational lower and upper bounds representing a single real number.”Computableℝ(def; a main declaration), declared in LeanPool/ComputableReal/ComputableReal.lean, line 27: “The quotient of interval-Cauchy sequences by equality of value, an ordered field whose ring operations are executable interval arithmetic.”IsComputable(class; a main declaration), declared in LeanPool/ComputableReal/IsComputable.lean, line 38: “A typeclass packaging an explicit interval-Cauchy approximation of a real number, used to drive its classical comparison instances.”Computableℝ.instField(instance), declared in LeanPool/ComputableReal/ComputableReal.lean, line 251: “The field instance on the quotient; inversion extracts a sign witness classically and is noncomputable.”ComputableℝSeq.Sqrt.sqrtq(def), declared in LeanPool/ComputableReal/SpecialFunctions/Sqrt.lean, line 136: “Computes converging rational interval bounds for the square root of a rational interval.”
Project
- Authors: Alex Meiburg.
- Source: doi:10.1007/978-3-540-71067-7_21, arXiv:0805.2438.
- Project repository: Timeroot/computableReal.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 65G40, 68V20.
- In Lean Pool: LeanPool/ComputableReal, from the card LeanPool/projects/computablereal.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.