Search. Organize.
Understand. Synthesize.
An automated AI4S platform for frontier scientific research.
Work ledger
Research In Progress
Active proof and disproof work, kept close to the evidence instead of buried inside announcements.
OEIS / Lean 4 / counterexample search / formalization
OEIS A237271 · Conjecture 2
The number of parts in the symmetric representation of σ(n) equals the count of 2-dense divisor sublists. Fully formalized in Lean 4 — zero sorry, no extra axioms, compiles clean.
OEIS A248802 · Conjecture 5
Disproved A248802(138n+6) = 1669 by counterexample: at n=51, index 7044, the value 1399 divides 2^(2^7044+2)+3, so A248802(7044) ≤ 1399 < 1669.
OEIS A241898 · Conjecture 0
Disproved the claimed lower bound a(n) > 7 for all n > 599: the value n = 736 = 4² + 12² + 24² yields a(736) = 4, a clean counterexample.
OEIS A281009 · Conjecture 1
Human-readable proof complete; the Lean formalization still carries one sorry. The machine-checked version is being finished now.
Problem atlas
Puzzle List
A compact inventory of scientific problems where AI systems can create leverage through search, simulation, proof, or experimental design.
45 puzzles / 5 domains / cost bands / method hypotheses
OEIS Remaining ~450 Open Conjectures
AlphaProof Nexus proved 44/492; ~450 integer-sequence conjectures remain
Erdős Open Problems (~670)
1179 problems documented, ~59% still open — combinatorics, number theory, graph theory
Frankl Union-Closed Sets Conjecture
In a union-closed family, at least one element appears in ≥ half the sets
Ramsey Number Exact Values
R(5,5) still unknown (known: 43–46); improving small Ramsey number bounds
Lonely Runner Conjecture
k+1 runners at distinct speeds on a unit circle each have a moment ≥ 1/(k+1) from all others
Erdős–Straus Conjecture
4/n = 1/x + 1/y + 1/z has positive integer solutions for all n ≥ 2
Graceful Tree Conjecture
Every tree admits a graceful labeling
Peaceable Queens
Maximum equal-count non-attacking black and white queens on an n×n board
Reconstruction Conjecture
A graph is uniquely determined by its vertex-deleted subgraphs
Navier-Stokes Singularity Search
Do 3D Navier-Stokes equations develop finite-time singularities? A Clay Millennium Problem
Turbulence Closure Problem
Unresolved turbulence closure models; DNS cost scales as ~Re³
Glass Transition
Mechanism of dynamical slowdown in liquid→glass transition — 'the deepest unsolved problem'
High-Temperature Superconductivity Mechanism
No consensus on cuprate microscopic mechanism; room-temperature SC unrealized
Quantum Many-Body Problem
Many-particle wavefunctions live in exponentially large Hilbert spaces
Quantum Spin Liquids
Disordered magnetic states at absolute zero; experimental confirmation remains difficult
Dark Matter Distribution Mapping
~27% of the universe's mass-energy, unobservable directly
Quantum Error Correction Decoding
Real-time decoding of surface-code syndromes faster and more accurately than algorithmic decoders
Neutrino Mass Ordering
Whether the neutrino mass spectrum is normal or inverted remains experimentally undetermined
DFT Exchange-Correlation Functional
The exact XC functional has never been found; all practical DFT uses approximations
Crystal Structure Prediction
Predicting crystal structure from composition — energy surfaces have astronomical minima
Universal Machine Learning Force Fields
MLFFs must balance accuracy, speed, transferability, and long-range interactions
Inverse Materials Design
Given target properties → generate materials; highly nonlinear mapping
Fully Automated Retrosynthesis
Given a target molecule → find optimal synthesis route; combinatorial explosion
Catalytic Reaction Mechanism Prediction
Predicting complete reaction mechanisms — bond breaking/forming order, transition states
Solid-State Battery Electrolyte Discovery
Finding solid electrolytes with ionic conductivity ~10 mS/cm
Protein-Ligand Binding Affinity Prediction
Accurate, generalizable prediction of small-molecule binding affinity to proteins is still unsolved
MOF Discovery for Gas Capture
Designing porous metal-organic frameworks with target porosity and capture performance on demand
Connectome → Function Mapping
Full fruit fly brain connectome complete, but structure→function gap remains
Non-Coding DNA Function
98% of genome function unknown — contains enhancers, silencers, and more
Intrinsically Disordered Proteins
~30% of residues lack stable structure, beyond AlphaFold's single-conformation reach
Protein Dynamics & Conformational Changes
Multi-state protein conformations determine activity under different conditions
RNA 3D Structure Prediction
Known RNA structures are an order of magnitude fewer than proteins
Cell Fate Determination
Is Waddington's landscape static or dynamic? Noise-driven or signal-driven differentiation?
Genotype–Phenotype Mapping
GWAS variants explain only a fraction of heritability
Splicing Code
Predicting which splice isoform is expressed in a given tissue
Aging Prediction & Mechanisms
Causal mechanisms of aging clocks, not just correlative markers
AMOC Tipping Point Prediction
Will the Atlantic Meridional Overturning Circulation collapse — and when?
Aerosol–Cloud Interactions
Largest source of uncertainty in climate models
Earthquake Prediction
Accurately predicting time, location, and magnitude remains unsolved
Species Extinction Risk Prediction
6th mass extinction — over half of data-deficient species are threatened
ENSO Prediction Beyond the Spring Barrier
El Niño/La Niña forecasts collapse across the boreal-spring predictability barrier, limiting lead times
Antarctic Ice-Sheet & Sea-Level Projection
Marine ice-sheet instability makes the upper bound of 2100 sea-level rise deeply uncertain
Space-Weather / Geomagnetic Storm Prediction
Forecasting solar flares, CMEs and geomagnetic storms that threaten satellites and power grids remains unreliable
Methane Super-Emitter Source Attribution
Pinpointing which facilities drive the disproportionate methane plumes seen from space is largely unsolved
Equilibrium Climate Sensitivity Constraint
How much warming a CO₂ doubling causes is still only bounded to a wide ~2.2–4.7 K range after 45 years