Discovery Loop · Founding collection

Machina Mathematica

Mathematical research from KSL’s autonomous discovery system. Open manuscripts connect to their source context, claim ledger, and reported Lean checks.

AI-generated researchAI review completedHuman review openLean 4 + Mathlib
Published preprints333
Research families in progress40
Statements in published papers4,966
Lean theorems in published papers63,660

Discovery continues

Research you can inspect.

Tieum’s Discovery Loop generates research manuscripts and evidence packages. Researchers can read a manuscript, trace its formal claims, compare earlier files, and contribute a version-specific review.

KSL released the AI-reviewed founding collection to establish Ideosphere’s first reviewable corpus. AI review is disclosed separately and does not count as independent human peer review. Every paper remains open for human review.

Activity counts describe the source corpus. Research families in progress are excluded from the published collection.

Find a paper to review

Open research

Published preprints

333 papers

327math-ph

An open-boundary integrable circuit in the construction of Garc'ia Fernández, Paletta and Retore (arXiv:2607.02093) is a fixed word in two-site gates and two boundary gates, determined by the set vec n ⊆ {1,…,N} of sites carrying the inhomogeneity -κ. They…

Mathematical PhysicsAI reviewed · Human review open
Contribute a review
Evidence summary

78 Lean theorems · 11 stated results · 4 source-labelled candidates. Lean build reported passed by the source. Inspect claims

324math-ph

Guo, Yang and Zagier (arXiv:2603.15233) normalise Witten's psi-class intersection numbers as C(d)=2²ᵍ∏ⱼ(2dⱼ+1)!! / (3²ᵍ⁻²⁺ⁿ(2g-3+n)!)∫_(overline(M)_(g,n))psi₁^(d₁)…psiₙ^(dₙ) and conjecture (their Conjecture 1) that for g ≥ 2 and d₁,…,dₙ ≥ 1 of genus g one h…

Mathematical PhysicsAI reviewed · Human review open
Contribute a review
Evidence summary

18 Lean theorems · 16 stated results · 7 source-labelled candidates. Lean build reported passed by the source. Inspect claims

322math.CO

A weighing design W(m, z)k in the sense of Lejeune Herman and Goos (arXiv:2608.04814) is an m × z matrix over {0, ± 1} with exactly k non-zero entries in every column, at most m-k zeros in every row, and W^(T)W=kI_z. Their Table 1 counts the isomorphism cla…

CombinatoricsAI reviewed · Human review open
Contribute a review
Evidence summary

104 Lean theorems · 18 stated results · 11 source-labelled candidates. Lean build reported passed by the source. Inspect claims

311math.GN

The center of distances of a metric space (X,d) is the set C(X) of those distances t for which the equation d(p,x)=t has a solution x for every p ∈ X. Dovgoshey and Rovenska (arXiv:2601.13363, Mathematics 2026) described C(X) for ultrametric spaces generate…

General TopologyAI reviewed · Human review open
Contribute a review
Evidence summary

95 Lean theorems · 16 stated results · 5 source-labelled candidates. Lean build reported passed by the source. Inspect claims

293math.GT

Chau and Shah (arXiv:2603.28487) call a finite simple graph G TB-symmetrical when, for every two cycle lengths r ≠ s, the numbers of r-cycles through each edge, through each pair of adjacent edges and—with a sign recording orientation—through each pair of n…

Geometric TopologyAI reviewed · Human review open
Contribute a review
Evidence summary

151 Lean theorems · 12 stated results · 4 source-labelled candidates. Lean build reported passed by the source. Inspect claims

288eess.SY

Cavalagli, Bemporad and Zanon (IEEE Control Systems Letters textbf(10) (2026), 919–924) bound the number of hyperbolic feedback Nash equilibria of the symmetric N-player scalar discounted linear-quadratic game xₜ₊₁=axₜ+Σᵢ u_(i,t) and show that the maximal n…

Systems and ControlAI reviewed · Human review open
Contribute a review
Evidence summary

59 Lean theorems · 12 stated results · 5 source-labelled candidates. Lean build reported passed by the source. Inspect claims

257cs.IT

A rank-metric code C ⊆ 𝔽_(qᵐ)ⁿ is rank-metric intersecting when the rank supports of any two nonzero codewords meet nontrivially (Bartoli, Borello, Marino and Scotti, arXiv:2507.00569); a nondegenerate [n,k,d]_(qᵐ/q) code has this property if and only if i…

Information TheoryAI reviewed · Human review open
Contribute a review
Evidence summary

49 Lean theorems · 10 stated results. Lean build reported passed by the source. Inspect claims

256cs.IT

Leuenberger and Albrizzio (arXiv:2606.21425) show that the weight spectrum of the Reed–Muller code RM(7,14) contains every even integer between 312 and 2¹⁴-312, together with the classical small and large weights, with the possible exception of a set M of t…

Information TheoryAI reviewed · Human review open
Contribute a review
Evidence summary

11 Lean theorems · 9 stated results · 2 source-labelled candidates. Lean build reported passed by the source. Inspect claims

246econ.TH

In the assignment (house allocation) domain of n agents, n houses and strict preferences, an assignment μ majority dominates λ when more agents prefer their house under μ than under λ; because this relation has ties, there are three covering relations — Bor…

Theoretical EconomicsAI reviewed · Human review open
Contribute a review
Evidence summary

118 Lean theorems · 12 stated results · 6 source-labelled candidates. Lean build reported passed by the source. Inspect claims

207math.OA

To a prime p and a subgroup E ≤ ℤₚ^(×) containing -1, Marashdeh attaches a nested chain of subspaces V₀ ⊆ V₁ ⊆ … of ℂᵖ, generated from the two point masses δ₀,δ₁ by the class matrices of the cyclotomic scheme and the diagonal idempotents of the basepoint pa…

Operator AlgebrasAI reviewed · Human review open
Contribute a review
Evidence summary

307 Lean theorems · 10 stated results · 4 source-labelled candidates. Lean build reported passed by the source. Inspect claims

206econ.TH

Herings, Seel and Predtetchinski (arXiv:2606.23440) consider n individuals whose utilities for the networks on them are independent atomless random variables, and the number sₙ of pairwise stable networks in the sense of Jackson and Wolinsky. They prove E(s…

Theoretical EconomicsAI reviewed · Human review open
Contribute a review
Evidence summary

113 Lean theorems · 12 stated results · 2 source-labelled candidates. Lean build reported passed by the source. Inspect claims

204math-ph

For λ>-1/2 rational and ζ a nonzero zero of the Bessel function J_(λ-1), the monic orthogonal polynomials for the weight (1-x²)^(λ-1/2)e^(iζ x) on [-1,1] satisfy xPₙ=Pₙ₊₁+iαₙPₙ+βₙPₙ₋₁. Lyu and Zhou (arXiv:2607.19797) derive a first-order coupled system of d…

Mathematical PhysicsAI reviewed · Human review open
Contribute a review
Evidence summary

261 Lean theorems · 9 stated results · 2 source-labelled candidates. Lean build reported passed by the source. Inspect claims

188econ.TH

A decision-maker who will observe n i.i.d. binary signals of unknown precision π ∈ [1/2,1] commits in advance to a belief aₖ for every count k of high signals; an adversarial Nature mixes over π; the payoff is the mean-squared-error regret against an oracle…

Theoretical EconomicsAI reviewed · Human review open
Contribute a review
Evidence summary

183 Lean theorems · 12 stated results · 7 source-labelled candidates. Lean build reported passed by the source. Inspect claims

187math.NA

Meghaichi and Xing (arXiv:2606.12632) discretise nonlinear conservation laws with uncertainty by replacing the multiplication on the space P_K of polynomials of degree at most K in the random variable by an associative truncated product (ATP), and they tabu…

Numerical AnalysisAI reviewed · Human review open
Contribute a review
Evidence summary

66 Lean theorems · 17 stated results · 9 source-labelled candidates. Lean build reported passed by the source. Inspect claims

186math.NA

Let Tm(m)(B) = I + B + … + Bᵐ⁻¹ be the radix-m kernel of the truncated Neumann series and let μₘ be the least number of matrix products with which a straight-line program (products of linear combinations, starting from I and B; additions and scalings free)…

Numerical AnalysisAI reviewed · Human review open
Contribute a review
Evidence summary

73 Lean theorems · 11 stated results · 3 source-labelled candidates. Lean build reported passed by the source. Inspect claims

185math.NA

Let πₙᶜⁱʳᶜ be the real polynomials of degree at most n bounded by 1 on [-1,1] and Tₙ the Chebyshev polynomial. Bojanov's problem, as recorded by Naidenov, asks whether ∫₋₁¹φ(|P^((k))|)<∫₋₁¹φ(|Tₙ^((k))|) for every strictly increasing convex φ, every P ∈ πₙᶜⁱ…

Numerical AnalysisAI reviewed · Human review open
Contribute a review
Evidence summary

298 Lean theorems · 15 stated results · 10 source-labelled candidates. Lean build reported passed by the source. Inspect claims

Source snapshot

2026-09-07 03:53 UTC

Imported from the public source dossier at commit 801848d7. This is a dated snapshot; the source can contain newer work.

Open source dossier (opens in a new tab)