Research // what we found, and what we helped others find

Research

Our founding members’ own research, the work Aska Digital contributed to, and every repository behind them. Each piece says whose it is, what the people and the AI agents did, and how far the evidence goes. None of it has been through peer review yet, and each piece says so.

Not peer reviewed 6 projects · 5 founding members data/projects.json · 14 Oct 2026

How we work Founding members’ research Work we contributed to Every repository

Propose, check, decide: one project at a time

How to read: each project’s own numbers at the three steps every result here goes through: AI agents propose, checkers verify, people decide and sign. Choose a project, or press play to go through all six.

Ctrl //

Agents propose
7,459,491
repeating dips found by the first full-sky search in NASA’s public TESS data
src: eumemic/exoplanets README.md, full-sky search table
Checkers verify
13,986
of them matched no known planet or TESS Object of Interest and passed all 17 automated tests of LEO-Vetter, a published vetting tool
src: README.md, full-sky search table
People decide and sign
665
counted as planet candidates on 14 Oct 2026, each with predicted transit times anyone can test; none confirmed yet
src: README.md, note of 14 Oct 2026 (58c6318)

Exoplanets · eumemic, with AskaCandidates · not confirmedNot peer reviewedOpen Exoplanets

Sources: each station’s own line; numbers from data/projects.json and the project dossiers, checked 13–14 Oct 2026.

Show all six as a table

Each project at the three steps
Project	Agents propose	Checkers verify	People decide and sign
Exoplanets	7,459,491 repeating dips found by the first full-sky search in NASA’s public TESS data (eumemic/exoplanets README.md, full-sky search table)	13,986 of them matched no known planet or TESS Object of Interest and passed all 17 automated tests of LEO-Vetter, a published vetting tool (README.md, full-sky search table)	665 counted as planet candidates on 14 Oct 2026, each with predicted transit times anyone can test; none confirmed yet (README.md, note of 14 Oct 2026 (58c6318))
Integer multiplication below n log n	1,334 pull requests opened by people and their agents in the first week (git ls-remote refs/pull/*/head, 13 Oct 2026)	47 assembly inequalities the current record passes in exact arithmetic, with independent owner and pricing audits (CrocSwap/integer-mult-bounds README, PR #1094 review)	17 reviewed records selected by maintainer Doug Colkitt, 9 to 13 Oct; all conditional on the unreviewed manuscript (certificates/selected-result.json history (20 commits, 17 distinct values))
Incentre lattice	5 runs an AI search loop went from density 0.4686 to the Kepler bound 0.7405 in about 11 minutes (autoresearch-fold/results.tsv)	16,240 exact numbers, every one ≥ 0, that rule out a collision anywhere along the fold (3,248 pair tests) (results/fold-continuous-fcc/certificate.json)	v2 preprint published and signed by Ahraz Arifuddin on Zenodo, 13 Oct 2026; no person other than the author has checked the proofs yet (doi.org/10.5281/zenodo.23340326)
After the 722	722 manuscripts written by one OpenAI model, with about three hours of computing per result on average (openai/math README @ adc7f12 and fd4aeeb)	300 / 719 top-line results formalized in Lean by OpenAI’s own count on 7 Oct; its catalogue marks them unreviewed (openai/math history.md @ fd4aeeb)	3 manuscripts withdrawn by OpenAI on 7 Oct after a sign error; none refereed by people so far (openai/math history.md @ fd4aeeb)
mobius-x1	3 versions of the claimed theorem, researched and drafted with Claude (mobius-x1 README.md, NOTICE)	0 / 3,456,000 failures in Aska’s full-network check of Theorem 2; Lean checks the arithmetic core (certificates/run_e1_rep_h10_bad0.txt)	0 human referees so far; it was refereed only by AI agents, and says so (mobius-x1 README.md)
gf2m-circuits	112 gates for an AES-field multiplier at depth 6, found by a search that scores every candidate wiring by total gates (2010 record: 117) (papers/Jain_GF2m_multipliers_2026.pdf, Table 1)	65,536 input pairs every AES-field multiplier is tested on, all of them; 30 Lean proofs that circuits compute the right answer (their gate counts are not Lean-checked) (multipliers/tools/verify.py; multipliers/lean, sbox/lean)	2 papers posted in the repository by Swapnil Jain, who signs them; not peer reviewed (papers/ in the repository)

00//How we work

The same rule for people and machines

Agents propose. Checkers verify. People decide.

Every result on these pages went through the same three steps, and each one tells you which step it has reached.

AI agents propose, freely. An agent is an AI model set loose on a task: it reads, writes code, runs it, looks at what happened and tries again. Agents are cheap and do not tire, so we let them try far more ideas than a person could, and most of those ideas fail. A proposal costs almost nothing, so on its own it proves nothing.

Checkers verify, strictly. A checker is a program that accepts a claim only if it passes a test with no room for opinion: arithmetic done exactly, with no rounding; every case of a finite search, run to the end; or a proof checker such as Lean, which accepts a proof only if every single step follows from the rules. A checker does not care who, or what, made the claim.

People decide, and sign. A person picks the question, reads what the checker actually confirmed, decides whether that is the thing we meant, and puts their name to it. When something turns out to be wrong, a person answers for it.

Every claim carries its status. Each result wears a plain label saying how far it has climbed, such as CLAIMED, PREPRINT, CONDITIONAL, PEER REVIEWED or LEAN-VERIFIED. A claim is never dressed up as a proof, and a check of one step is never sold as a check of the whole.

Where each project stands

How to read: five rungs of evidence, weakest at the bottom. Each project sits on the rung of its headline claim, the weakest part of its status line; point at or focus a project for its full status.

Formally verified
A proof checker such as Lean accepted every step.
none of our projects yet
Independently replicated
Someone else did it again and got the same answer.
none of our projects yet
Peer reviewed, or deployed
Checked by outside experts, or in daily use.
none of our projects yet
Preprint, or conditional
Written out in public; or true if an earlier, unreviewed result is.
Incentre lattice Integer multiplication below n log n After the 722 gf2m-circuits
Claimed, or candidate
Someone says so, with evidence still to come.
Exoplanets mobius-x1

Source: each project’s status in data/projects.json. A project can have parts on higher rungs: the Fourier record inside “After the 722” is Lean-verified, and every gf2m-circuits circuit is Lean-proved to compute the right answer, though its gate counts and the comparisons with earlier records are not.

01//Founding members’ research

Point at or focus a card to run its figure

Four lines of work by founding members, all in the open.

Each card says whose work it is and exactly what Aska Digital added. Every number has its source beside it.

GeometryAhraz Arifuddin · Aska Digital

Incentre lattice

From a doodle to the densest packing of balls.

PreprintNot peer reviewed

Aska Digital’s own work. Founding member Ahraz Arifuddin chose the questions and signs the claims; AI models from Anthropic and OpenAI drafted most of the proofs, code and checks, and the paper records which model did what.

THE DOODLE, DRAWN EXACTLYr = (√2−1)/2 ≈ 0.2071

A square, its diagonals, one dot per triangle at its incentre (the centre of the circle that fits inside it). Neighbouring dots end up √2 − 1 apart.

22.3% → 74.05%space filled by the balls along the exact fold, from loose scaffold to the densest possible stacking, π/√18results/fold-continuous-fcc/certificate.json; PROOF.md
16,240exact numbers, every one ≥ 0, ruling out a collision anywhere along the fold (3,248 pair tests)results/fold-continuous-fcc/PROOF.md
1/(n²−n−1)how much the framework thins sideways when stretched, in every dimension n ≥ 3 (written proof, reviewed only by AI models)results/rigidity-nd/PROOF.md
~11 minfor an AI search loop to climb from 46.9% to the 74.05% ceiling, in 5 logged runsautoresearch-fold/results.tsv (07:56:10 to 08:06:56)

On Foundation0 Site Repository Preprint v2 (Zenodo)

Astronomyeumemic, with Aska

Exoplanets

Faint shadows in old starlight: 665 small-planet candidates in public NASA data, as of 14 Oct 2026.

Candidates · not confirmedNot peer reviewed

Founding member eumemic’s project, built with Claude Code. Aska sent ten merged pull requests, one of which built the first version of its website; one fix, restoring light curves the data reader had dropped (PR #6), led to a re-search that added 120 counted candidates.

SCHEMATIC · STACKING PASSES64 passes stacked

Why stacking works: noise shrinks like 1/√N as passes are added, until a dip too small to see once stands out. The dip is TIC 4206066’s published 398 ppm, 1.7 h signal; the noise is simulated.

4,039,203stars searched in the full-sky search, using every TESS sector from 1 to 104 (2018 to 2026)README.md, full-sky search table, at 58c6318
665planet candidates counted on 14 Oct 2026 (607 from the full-sky search, 58 from earlier ones); none confirmedresults_public/candidates_allsky.csv + tiers_earlier_candidates.csv at 58c6318
7,459,491 → 13,986repeating dips found; of them, those that matched no known planet or TESS Object of Interest and passed all 17 automated tests of LEO-Vetter, a published vetting toolREADME.md, full-sky funnel, at 58c6318
82%of the full-sky candidates checked are on stars seen only in wide-field images, which NASA’s multi-sector search does not covervalidation/findability.md (404 of 494, 13 Oct 2026)

On Foundation0 Site Repository

AlgorithmsDoug Colkitt + crowd

Integer multiplication below n log n

A public race of people and AI agents to multiply huge numbers in fewer than n log n steps.

Conditional · maintainer-reviewedNot peer reviewed

Founding member Doug Colkitt’s race (CrocSwap). Founding member rohanarun held the reviewed record on 14 Oct (PR #1094), and eumemic sent 80 pull requests. Aska built the live race tracker that grew into this site, and submitted two small claims that were never reviewed and were soon overtaken.

LOG₂ κ · DATED 23 SEP → 13 OCTlog₂κ −9.22

Every reviewed record on a halvings scale, from the machine-written paper’s 2⁻¹⁸² to 2^−9.22. All of them rest on that unreviewed paper.

0.001672660197076918reviewed κ, conditional, PR #1094 by founding member rohanarunsnapshot · 13 Oct 2026, 18:45 UTC (live file unreachable)
2⁻¹⁸² → 2^−9.22κ since the machine-written preprint dated 23 Sep 2026 (about 1.03×10⁵² times larger)src: upstream/build/sections/00-introduction.tex; log2 of selected κ (computed)
17successive reviewed κ records in 5 days (9–13 Oct)git log -- certificates/selected-result.json (20 commits, 17 distinct values)
1,334pull requests opened upstream by 13 Oct 2026 (highest #1374)src: git ls-remote origin refs/pull/*/head, 13 Oct 2026, about 23:40 UTC

On Foundation0 Repository Race tracker (feed of 11 Oct)The story

MathematicsMembers + crowd

After the 722

OpenAI published 722 machine-written maths papers. Here is what people and their agents did next.

Mostly conditionalNot peer reviewed

Starts from OpenAI’s 722 machine-written manuscripts. Founding members rohanarun and Ryan Shea took six of its families further within a week, and Doug Colkitt’s race a seventh; eumemic and many others joined in.

TIMES BETTER, LOG SCALE6 results

How many times better six numbers got in a week, on a log scale. Long bars mean loose first proofs, not important results.

722 → 719machine-written manuscripts on 6 Oct, then 7 Oct after three were withdrawnopenai/math README @ adc7f12 and fd4aeeb
372families of results; 242 link a Lean scope document (a plan for checking, not a finished check)data/openai-math-families.json
7families founding members built on within a weekdata/members.json builds_on
52public steps that tightened six results, 7 to 13 OctAfter the 722, section 03

On Foundation0 openai/math Math, faster (essay)

02//Work we contributed to

Swapnil Jain’s repositories

Two repositories by Swapnil Jain, with a part from us.

These are Swapnil Jain’s results. Aska’s agentic team sent one pull request to each, and each card says exactly what that pull request did.

CircuitsSwapnil Jain + Aska

mobius-x1

A claimed way to compute a basic transform on bits (the GF(2) Möbius transform) with fewer one-bit XOR steps than Yates’ 1937 recipe, for astronomically large inputs.

Not peer reviewed · AI-refereed only

Swapnil Jain’s repository. Aska wrote and ran the full-network check behind Theorem 2, its strongest version: 3,456,000 bank swaps tested in a network of size h = 10, with zero failures (merged PR #1).

PASCAL MOD 2 · 32 INPUTSrow 31 · 32 odd

The matrix the transform computes, made here from Pascal’s triangle with the odd entries filled. The claimed saving only appears when the input has billions of digits.

4.37 × 10⁻¹¹how far below 1 the claimed exponent drops: N·(log N)^θ′ with θ′ = 1 − 4.3713·10⁻¹¹ (Theorem 2)README.md; Lean bound in lean/MobiusLean/Prepass.lean
0 / 3,456,000failed checks in Aska’s full run of the network at label size h = 10 (all 43,200 runs of the step)certificates/run_e1_rep_h10_bad0.txt
92supporting theorems checked by Lean; the main theorem is not one of themlean/axioms.out
0human referees so far; AI referees read it (2 for Theorem 1, 1 each for Theorems 1′ and 2)docs/RESULT.md

On Foundation0 Repository Aska PR #1

CryptographySwapnil Jain + Aska

gf2m-circuits

Fewer logic gates (the tiny on/off circuits chips are built from) for the arithmetic inside AES, the cipher that protects most web traffic.

Lean-verifiedTested on every inputNot peer reviewed

Swapnil Jain’s repository. Aska contributed verified multipliers for four more binary fields, built with the papers’ method (merged PR #1); they are not records.

GATES vs DEPTH · AES FIELD−5 gates at depth 6

Each new multiplier is checked on all 65,536 input pairs and proved in Lean. Hollow mark: the 2010 record.

117 → 112gates to multiply in the AES field at the 2010 record’s depth (6); 107 if depth 13 is allowed (Jain 2026)papers/Jain_GF2m_multipliers_2026.pdf Tables 1–2; re-verified with multipliers/tools/verify.py
106gates for the AES S-box from AND, XOR and XNOR gates (Jain 2026, depth 24; the smallest found before was 110 at depth 22, NIST 2026)papers/Jain_AES_Sbox_circuits_2026.pdf Table 1; sbox/verify_results.txt
109gates for the inverse AES S-box (Jain 2026, depth 30; NIST 2026: 112 at depth 26)papers/Jain_AES_Sbox_circuits_2026.pdf Table 1; sbox/verify_results.txt
30Lean 4 proofs that a circuit computes the right answer (19 multipliers, 11 S-boxes); gate counts and depths are not Lean-checkedmultipliers/lean, sbox/lean and their .out files

On Foundation0 Repository Aska PR #1

03//Every repository, by member

No portraits, by design

Everything each founding member has on the record.

Five people who already work this way, and the repositories behind their work. “Builds on” names the family of OpenAI’s machine-written manuscripts a repository starts from.

Show //

22 of 22 entries

M·01

Ahraz Arifuddin

@ahrazzle

Runs Aska Digital's team of AI agents and points it at open questions. The main project follows a childhood doodle (a square, its diagonals, one dot per triangle) into crystal geometry, ending in an exact proof that a loose ball-and-rod scaffold folds, without stretching, into the densest stacking of equal balls.

Main projectIncentre lattice

Incentre lattice
PreprintNot peer reviewed
Exact fold from density 0.2233 to 0.7405 (the Kepler bound), with 16,240 exact certificate coefficients.
On Foundation0Incentre lattice
Exoplanets: pipeline fixes and website
Merged · credited
Ten merged pull requests to eumemic's search: four pipeline fixes, one of which (PR #6) led to a re-search that added 120 counted candidates; an independent check; tests; documentation; and the first version of the project website.
On Foundation0Exoplanets
mobius-x1: full-network check
Merged
The whole-network test behind Theorem 2: 0 failures in 3,456,000 checks.
On Foundation0mobius-x1
gf2m-circuits: field multipliers
Merged · not records
Verified multiplier circuits for more binary fields, e.g. GF(2⁹) in 136 gates against a 142 baseline.
On Foundation0gf2m-circuits
Foundation0
This site
Began as a live tracker of the integer-multiplication race.

M·02

eumemic

@eumemic

Builds software for long-running AI agents and puts those agents to work on open science. The main project, built with Claude Code, searched NASA's public TESS data for more than four million stars and as of 14 October 2026 counts 665 small-planet candidates too faint to see in any single month of data.

Main projectExoplanets

Exoplanets
Candidates · not confirmed
4,039,203 stars searched; 665 candidates as of 14 Oct 2026.
On Foundation0Exoplanets
Integer-multiplication race
Conditional · maintainer-reviewed
80 of the first 722 pull requests inventoried in the race's PR ledger (13 Oct 2026); on 13 Oct the record's bit block built on their #555.
On Foundation0Integer multiplication
Builds onOpenAI family 109: Integer multiplication below n log n
exact-dft-bounds
Claimed · superseded
Exact Fourier transforms below n log n with saving 4.856×10⁻⁴; held the best claim for about six hours.
Builds onOpenAI family 130: Exact Fourier transforms below n log n
rlmath
In progress
A test bench for training an AI to split Lean theorems into lemmas a smaller prover can finish.

M·03

Doug Colkitt

@Mister-Meeseeks

Started and maintains the open race to multiply huge numbers in fewer than n log n steps, the best speed proven so far. People and their AI agents took a machine-written paper's saving of 2⁻¹⁸² and grew it to about 2^−9.2 in a week, every step checked in exact arithmetic, all still resting on the unreviewed original paper.

Main projectinteger-mult-bounds

integer-mult-bounds
ConditionalNot peer reviewed
Creator and maintainer; κ from 2⁻¹⁸² to 0.00167266 (PR #1094, 13 Oct 2026).
On Foundation0Integer multiplication
Builds onOpenAI family 109: Integer multiplication below n log n
erdos-875-carry-lemmas
Partly Lean-verifiedNo human review
One model proves, a rival model attacks: a sharp carry lemma behind the best construction for Erdős Problem 875. Not a resolution of the problem.
Gradients to ChatGPT (g2c)
Course
A build-it-yourself course on how language models work.

M·04

rohanarun

@rohanarun

Builds software that lets AI coding agents work on open research problems, including Auto-research-agent, a Mac app that sends Codex or Claude Code to an open problem in one click. With those agents, the most active contributor to the integer-multiplication race, and the author of conditional refinements to four of OpenAI's machine-written papers.

Main projectAuto-research-agent

Auto-research-agent
Released software
A native Mac app: one click sends your own coding agent, or several in parallel, to an open problem.
On Foundation0Instruments: Auto-research-agent
Integer-multiplication race
Reviewed record on 13–14 Oct 2026Conditional · maintainer-reviewed
142 pull requests as of 14 Oct 2026; PR #1094 was the reviewed record on 13–14 Oct 2026 (κ = 0.001672660197076918).
On Foundation0Integer multiplication
Builds onOpenAI family 109: Integer multiplication below n log n
van-der-waerden-refinement
ConditionalNo human review
The constant in OpenAI's van der Waerden bound rose from 1/100000 to 1/9, jointly with other contributors.
Builds onOpenAI family 160: Superexponential van der Waerden numbers
sidorenko-template-refinements
Exact certificatesNot peer reviewed
No smaller certificate than OpenAI's 35-vertex counterexample exists inside its template; one constant cut from 1641 to 189.
Builds onOpenAI family 161: Counterexamples to Sidorenko’s conjecture and the forcing conjecture
matrix-multiplication-sector-barrier
Proof + exact testsNot peer reviewed
Shows where one step of OpenAI's 9/4 matrix-multiplication method must stop.
Builds onOpenAI family 107: Matrix multiplication with exponent at most 9/4
unit-distance-grid-refinement
ConditionalNot peer reviewed
Shrinks the final grid in OpenAI's unit-distance proof from 20×5 to 8×4.
Builds onOpenAI family 167: Planar distinct distances and unit-distance bounds
integer-multiplication-illustrated
Exposition
An illustrated reading guide and annotated edition of OpenAI's integer-multiplication paper.
Builds onOpenAI family 109: Integer multiplication below n log n

M·05

Ryan Shea

@shea256

Builds tools for AI-run experiments, such as autofoundry, which rents GPUs from four cloud providers and runs the same experiment across them. Working with Codex and Claude on OpenAI's machine-written problems, they ranked first, as of 14 Oct 2026, on a public board for exact Fourier transforms below n log n, with a Lean-verified result shared with Jeremy Kothe, whose circuit it uses.

Main projectautofoundry

autofoundry
Open-source software
Rents GPUs across RunPod, Vast.ai, PRIME Intellect and Lambda, runs one experiment everywhere, reports best, mean and worst.
On Foundation0Instruments: autofoundry
fourier-transform-below-nlogn
Lean-verifiedHuman review pending
Exact Fourier transforms of any length in O(n (log n)^1−δ) steps with δ = 0.0012331685; rank 1 on the Big O Speedrun board as of 14 Oct 2026, shared with Jeremy Kothe.
Builds onOpenAI family 130: Exact Fourier transforms below n log n
matroid-prophet-inequality
Written proof + exact certificatesNot reviewed
Raises a guaranteed fraction in the one-sample matroid prophet problem from 2⁻²⁹³ to above (35/32)·2^−31.
Builds onOpenAI family 111: One-sample matroid prophet inequalities against an almighty adversary

Source: data/members.json (names as each member shows them on GitHub or in their own published work; status lines as each repository states them). Member pronouns: they/them.

04//Sources

Report an error and we fix it in the open

Where this page comes from.

Projects, statuses and numbers: data/projects.json; each number’s own source file or commit is printed beside it on its card.
Founding members and their repositories: data/members.json.
OpenAI’s 372 result families and our field classification: data/openai-math-families.json, from openai/math.
The reviewed κ of the integer-multiplication race is fetched live from certificates/selected-result.json when you open this page; if that file cannot be reached, the card falls back to the newer of this site’s own feed.json and our dated snapshot, and says which it shows and when.
Mistakes: open an issue. Corrections are made in public, in the repository history.