Echea

Superintelligence Research Lab at the Frontier of Deterministic Algorithms

Superintelligence Research Lab replacing Guesswork with Math

General: LLM Design: Chip Design:

Copied

A New Paradigm

Formal Reasoning for Superintelligence

Formal Reasoning: No Guessing

We are building the world's fastest SAT Logic Solvers: deterministic algorithms for NP-Complete problems at industrial scale.

Formal Reasoning and Mathematics allow us to find solutions in exponential combinatorial spaces with zero errors, no approximations, and perfect efficiency.

No more induction. Now is the age of deduction.

Today's AI is expensive and approximate. It guesses billions of times and still only lands on a "good enough" answer.

We use math to calculate the best answer directly, in one step. You send us the problem. We return the exact answer. Every tool built on top of us gets faster, cheaper, and provably correct.

The same math cracks chip design, trading, and drug discovery, so we sell real products on the way to becoming a frontier lab.

NP-Completeness

One Problem Class. Every Industry.

One Math. Every Industry.

Chip placement, supply chain routing, molecular search, order scheduling, and neural-network training are all NP-Complete problems. The same exponential search space appears in every critical system.

We are building a universal API and MCP layer that exposes exact, deterministic algorithms for this shared problem class. One endpoint, every industry, because it is the same puzzle underneath.

Chip layouts, supply chains, drug molecules, trading portfolios, and AI training are all the same puzzle underneath.

We are building one universal API, an MCP-style layer. Chip designers send layouts. Quant firms send order books. Pharma teams send molecular spaces. Every one gets back the exact, optimal answer.

Solve the puzzle once, sell it everywhere.

Scaling Laws

SAT Scaling Laws

Self Recursive Intelligence

Two scaling laws define the trajectory of AI: deterministic (Algorithms) and empirical (Data+Compute+Algorithms).

SAT solvers themselves have gotten roughly 10,000× faster since the 1980s driven by algorithmic breakthroughs. Yet empirical scaling has still outpaced that curve for the last Two decades. The deterministic curve is self-improving: each generation of the algorithm produces a mathematically verified speedup over the last, compounding without the stochastic variance of empirical scaling.

Can math really beat bigger computers? It already has.

Since 1980, the math side has delivered a 10,000× speedup on the core problem AI is built on, with zero new hardware.

And the algorithm is self-improving. Every new version is mathematically proven to be faster than the last, no guessing involved. That curve keeps going.

1980 – 2005: Math wins.
2005 – 2026: Bigger computers win.
2026 onwards: Math wins again.

The Hardest Problems

Beyond Gradient Descent

Darts in the Dark

The industry settled on a training paradigm that works. The first paradigm was about getting something to work. The next is about finding out why it works. One must just look in the right places.

Guesswork and Approximation.
Messy and Expensive.

Gradient descent is a step by step method.
Time must be used.

But why not simultaneously?

Training AI today is like throwing darts in the dark.

Billions of small adjustments. Trillions of dollars in computers. And you never get the best answer, only an acceptable one.

Every AI company is built on this guessing method. The wall is here.

The Frontier Paradigm Shift

The Middle Ground

Math Trains the Machine

AI has long swung between two poles: symbolic AI, rule-based and deterministic but brittle at scale, and stochastic AI, powerful but probabilistic and fundamentally unverifiable.

We have found the middle ground. Formal reasoning does not replace neural networks. It trains them.

Today's AI. Approximate. Expensive. Unverifiable.

Echea. Exact. Efficient. Mathematically proven.

The math does not replace neural networks. It trains them.

Becoming a Frontier Lab Algorithm · Software

Pre-Training Reversed

Name the Destination

We reverse gradient descent. Rather than descending toward a minimum, we specify a target loss L* and reverse-find every input x* that achieves it. No more stochasticity.

Today's training takes millions of small steps downhill, hoping to land somewhere good. Each training run costs tens of millions of dollars.

We skip the walk. Name the destination: the quality of model you want. Our math tells you exactly which weights get there, in one step.

Optimization as a Service Compute · Hardware

Chips Perfected

The Silicon Puzzle, Solved

We solve placement and routing at silicon scale, bin-packing billions of transistors into minimal area while finding optimal signal routes across metal layers.

Laying out a chip is a puzzle with billions of pieces. Today's tools throw darts at the board and leave 5–15% of the silicon wasted on every chip.

We solve the puzzle exactly. On a single $300M tape-out, even a 3% improvement is $9M saved, multiplied by every chip family, every year.

Publications

Research & Theory

The Work, In Public

A growing library of the publically-released papers that document our work on formal reasoning, deterministic algorithms, and the mathematical foundations of superintelligence.

The papers we have released publicly, showing the math behind everything above.

Appendix

Team

Jonathan Belay

Founder & CEO

Harvard CS '22. Founder of the first AI club at Harvard. Google Connectomics team, pre-training.

Simeon Radev

Co-Founder & CTO

Harvard CS '22. MIT for AI on NP-Complete protein folding. Etched for NP-Complete chip design.

William Shen

Biopharmaceutical Advisor

Harvard MCB '22. Harvard Med for NP-Complete drug design.

Henry Bosch

Mathematical Advisor (Terms being finalized)

Harvard CS '22. Stanford PhD in Math & CS. Etched for NP-Complete chip design. Lead Organizer of the Stanford PhD Seminar on Math & Computation.

Appendix

Academic Mentor

The leading expert researcher in our domain of computational complexity (#P Completeness), machine learning theory, and the mathematical foundations of computing.

Leslie Valiant

Turing Award Laureate · T. Jefferson Coolidge Professor of Computer Science and Applied Mathematics, Harvard University

He advises us informally and stays engaged with our theoretical progress.

Appendix

Angel Investors

Early backers committed to the deterministic paradigm.

Fei-Fei Li Co-Director, Stanford HAI · Founder, World Labs
François Chollet Creator of Keras · Co-founder, ARC Prize
Mike Knoop Co-founder, Zapier · Co-founder, ARC Prize

Appendix

Go-to-Market Strategy

Chip design is our focus. That is where a 10× speedup is worth the most today, and where our first commercial contract will land. Quant trading and pharma are adjacent markets we expand into once the chip-design solver is in production.

01
Priority · Now
Chip Design, Placement & Routing

Land with a top-5 fabless semiconductor customer; close the existing EDA tool gap on advanced nodes where current heuristics leave 5–15% area on the table.
02
Down the Line
Quant Trading, Order Scheduling

Partner with a tier-1 systematic trading firm to replace heuristic scheduling of order routing / execution flow, where deterministic guarantees are a regulatory and alpha advantage.
03
Down the Line
Pharma, Molecular Optimization

Apply deterministic combinatorial search to protein folding and drug target discovery pipelines, where exact answers cut trial-and-error cycles by orders of magnitude.

Target partners LOI TBD

Appendix

Product & Pricing

01

API Access

Per-solve pricing against a committed spend floor. Anchor customers commit $100K to $500K per year. Right tier for pilots, smaller workloads, and adoption inside customer R&D teams.
02

Enterprise License

Annual contract for unlimited production use. Target range: $1M to $10M per year, sized by customer scale and call volume. This is where most beachhead revenue will sit.
03

Embedded Solver

Integrated into customer infrastructure for silicon-scale call volume. Multi-year contracts, $5M to $25M, reserved for the largest customers running production workloads at scale.

Top-5 fabless tape-outs run $100M to $500M+. Heuristic placement-and-routing wastes 5 to 15% of silicon. A 3% improvement on a $300M tape-out saves $9M per family, per year. For a chip company running multiple tape-outs, a better solver is an eight- to nine-figure budget line.

Appendix

Market Size

SAT solvers have become roughly 10,000× faster from the 1980s to today driven by algorithmic breakthroughs, not Moore's Law. That curve hasn't flattened. Each new order of magnitude unlocks a dramatically larger market.

SOM · 10× + Tooling $10B

SAT + CUDA-style dev platform

A 10× SAT solver plus a CUDA-style developer ecosystem captures formal verification, EDA, and constraint-programming tooling.

SAM · 100× Faster $200B

Combinatorial optimization × ML

100× speedups open the full combinatorial-optimization stack, scheduling, routing, and discrete optimization inside machine learning.

TAM · 10,000× Faster $2.5T+

Replacing gradient descent & the GPU economy

At 10,000× speedups, deterministic solvers replace gradient descent and absorb the AI infrastructure spend currently going to stochastic search.

Appendix

Requirements

Funding for the team and compute we need to bring the deterministic paradigm from theory to industrial deployment.

5-10 Engineers Systems-minded engineers who can work vertically across the abstraction layers of a CUDA-style solver stack: each developing a different component end-to-end.
2 Theorists Algorithm designers to extend the mathematical core: new decomposition theorems, tighter bounds, and the next generation of deterministic methods.
2 Partnerships Operators embedded with chip-design and quant-trading customers to take the solver into production at real industrial workloads.
Compute GPU and cluster capacity to test many variations of the practical algorithm implementations. As we are close to the end, we can just brute force many of this now.

Appendix

Roadmap

Three phases over the next 18 months, each landing a concrete milestone: a SAT solver, an EDA-benchmark win, and the first deterministic foundation model.

Phase 1

SAT Solver, Summer 2026

Ship the deterministic SAT solver and publish benchmarks against state-of-the-art.
Phase 2

ISPD, Placement & Routing

Compete at ISPD with a deterministic placement engine; target a top-ranked submission.
Phase 3

Foundation Model Design

Design a foundation model trained with reversed gradient descent: the culmination of Phases 1 and 2.
Phase 4

Deterministic Superintelligence

Scale the deterministic paradigm across verticals, while expanding out the exact solvers

Appendix

An Expanding Frontier

This is a new category of AI research, and it is very early. The major labs have poured tens of billions into scaling stochastic methods. Labs focused on Formal Reasoning and Mathematics are only beginning. The space is wide open.

The major labs have called this direction too hard. That is precisely what makes the returns asymmetric. Echea is built to be the flagship lab of this frontier.

Appendix

Executive Summary

Thesis

Echea builds deterministic SAT solvers and #SAT (model counting) algorithms grounded in algebraic graph theory, spectral graph theory, and algebraic topology , replacing heuristic stacks with mathematical structure.

Team

Jonathan Belay, Founder & CEO. Harvard CS; founder of Harvard's first AI club; Google Connectomics (pre-training).
Simeon Radev, Co-Founder & CTO. Harvard CS; MIT (AI for NP-Complete protein folding); Etched (NP-Complete chip design).
Henry Bosch, Mathematical Advisor. Harvard CS; Stanford PhD Math+CS; Etched; organizer of the PhD Seminar on Math and Computation.
William Shen, Biopharmaceutical Advisor. Harvard CS; Harvard Med (NP-Complete drug design).
Leslie Valiant, Academic Mentor. Turing Award laureate; T. Jefferson Coolidge Professor of CS and Applied Mathematics, Harvard.

Traction

First research paper, Counting Vertex Covers in Trees (April 2026).
Technical memo, The Year Ahead (March 2026).
Leslie Valiant joining as Academic Mentor.

The Path to a 10× Business (Base Case)

Track record: SAT solvers have become roughly 10,000× faster from the 1980s to today, driven by algorithmic progress, not Moore's Law. Each decade has compounded 10×.
A 10× improvement on state-of-the-art is well within the historical trend and is the conservative near-term target.
Wrapped in a CUDA-style developer ecosystem (libraries, compilers, benchmarks, tooling), this captures a $10B+ SOM: EDA formal verification, constraint programming, reliability analysis, industrial scheduling and quant-trading order execution.
Beachhead customers: top-5 fabless semiconductor firms (placement & routing) and tier-1 systematic trading firms (order scheduling). Both have clear ROI on single-digit-million contracts.
This alone is a reasonable, venture-scale business with defensible IP and a mathematical moat.

The Path to a 10,000× Business (Upside Case)

Modern SAT solvers, like modern ML, are dominated by heuristics (CDCL, clause learning, variable ordering, restarts). Heuristics plateau.
#SAT opens a door heuristic-only solvers cannot: algebraic graph theory, spectral graph theory, and algebraic topology offer structural invariants and closed-form decompositions that expose the hidden geometry of combinatorial problems.
If that mathematical toolkit yields even polynomial structure on important instance classes, speedups compound far past 10×:
- 100×, full combinatorial-optimization stack (logistics, scheduling, hyperparameter & neural-architecture search, feature selection). ~$50B SAM.
- 10,000×+, deterministic solvers displace gradient descent for foundation-model training, replace heuristics across chip design, and absorb AI infrastructure CapEx currently spent on stochastic search. $1T+ TAM.
The upside case is a real frontier: the major labs have written it off as too hard. That is precisely what makes it asymmetric, if it works, the payoff is category-defining.

The Ask

5 engineers working vertically across the abstraction layers of a CUDA-style solver stack.
2 theorists designing algorithms (decomposition theorems, bounds, next-generation deterministic methods).
2 partnership leads embedded with chip-design and quant-trading customers.
Compute for running many variations of practical algorithm implementations.

Common Objections (Addressed)

“The SAT solver market is too small.”

The pure SAT-solver licensing market today is roughly $1B. That number is a red herring: it measures revenue generated by today's solvers on today's workloads, a function of solver capability, not of latent demand.

Consider the machine learning analog. In 2012 the commercial neural-network market was a rounding error. Computer vision, NLP, audio, robotics, drug discovery, and recommendation all relied on handcrafted features and shallow classifiers, because deep-network training was intractable at scale. Once GPU training became practical, ML did not merely grow the 2012 market, it absorbed every adjacent category. Those fields collectively became a multi-hundred-billion-dollar ML market almost overnight.

A 10× SAT speedup triggers the same dynamic in every industry that currently accepts heuristic output because exact methods are too slow: EDA placement and routing, supply-chain planning, quant order scheduling, protein folding and drug design, compiler optimization, constraint-based manufacturing scheduling. The addressable market is the entire optimization stack, not today's licensing pool. The $10B SOM framing is conservative; the TAM is every industry presently paying an optimality tax.

“P ≠ NP, so this is fundamentally impossible.”

Echea does not claim P = NP as a theorem. That problem is formally open, and nothing we are building depends on resolving it.

But the informal intuition behind this objection, "NP-hard problems must remain intractable on practical instances", has been materially weakened by empirical evidence, and investors should update accordingly.

First, the direct historical evidence. Since 1980, SAT solvers have improved by roughly 10,000× on industrially relevant instance classes. The CDCL revolution alone delivered several orders of magnitude without touching P vs NP. These gains came entirely from exploiting the fact that most real instances of NP-hard problems have hidden polynomial structure that worst-case complexity theory ignores. The trend shows no sign of saturating.

Second, the recent AGI signal. The rise of AGI-class systems provides an additional, and in our view under-appreciated, empirical update. Modern large models, which are bounded-size neural networks executing in polynomial forward-pass time, are now demonstrably solving or tightly approximating problems once considered to require exponential search: ad-hoc theorem proving, multi-step planning, combinatorial puzzle solving, code synthesis, and rough formal proofs. This is not a formal proof of P = NP. Worst-case complexity is untouched, and the theoretical question remains open. But it constitutes strong empirical evidence that the practical frontier between "polynomial" and "exponential" is far less strict than classical intuition suggested. Problems previously assumed to require exponential reasoning are routinely being solved, and in many cases exactly solved, by polynomial-size systems in polynomial time.

The rational update. Given the last five years of AGI progress, the informal prior that "NP-hard means practically intractable" is weaker today than at any point in the last fifty years. A careful Bayesian observer should update meaningfully toward the view that much more of NP has exploitable structure than the field has historically assumed, and that P = NP on practical instance classes, while still formally unproven , is now considerably more plausible as an empirical proposition than it was a decade ago. Echea is not betting on a proof. We are betting that a very large fraction of what we call NP-hard is effectively tractable once the right structural tools are brought to bear, and that the empirical case for that proposition is mounting every year.

“Stochastic methods / ML are winning. Why go deterministic?”

Heuristics and stochastic methods dominate today's AI landscape because rigorous alternatives did not exist at scale. That is not an argument against building rigorous alternatives, it is the reason to build them.

Entire categories are structurally inadmissible to stochastic methods:

Chip verification cannot tolerate probabilistic correctness. A fabbed logic bug on a 3nm node costs $100M+ to correct. Chip designers verify with SAT and SMT solvers, and will continue to.
Safety-critical systems (aerospace, medical devices, autonomous vehicles) increasingly require formal proofs rather than statistical guarantees. The FAA does not certify "trained probabilistic landing."
Cryptographic assurance is built on exact computation, not approximation.
Reliability analysis and probabilistic inference in structured domains reduce directly to #SAT. Stochastic sampling gives noisy estimates; #SAT gives exact counts.
AI alignment itself increasingly demands formal verification of agent behaviour, policy bounds, and value specifications. As models become more capable, probabilistic behavioural testing becomes insufficient; the field will need deterministic guarantees it does not currently have.

Stochastic and deterministic methods are complementary, not competitive. Echea is building the deterministic half of the stack , the half every scaled AI agenda will eventually need, and that nobody is currently building at industrial scale.

“Big labs will just build this themselves.”

They could, but they will not, and the pattern is well documented.

The frontier labs (OpenAI, Anthropic, DeepMind, Meta AI, xAI) have publicly committed enormous capital to scaling stochastic pre-training. Their technical leadership, compute, and roadmaps are structured around improving neural-network training efficiency, not around applying algebraic graph theory and algebraic topology to model counting. Their research output in #SAT and algebraic combinatorics is negligible.

Even if a frontier lab reallocated a pod to this area tomorrow, they would face a steep staffing problem. The combination of deep combinatorial and #SAT expertise, fluency in algebraic graph theory / spectral methods / algebraic topology, and CUDA-level systems engineering for industrial-scale solver implementation is exceptionally rare. Most people with the first two skills are in academia; most people with the third are at chip companies or high-frequency trading firms. Our team spans all three: Harvard CS theory, MIT research on NP-Complete protein folding, Stanford PhD in Math and CS, Etched chip-design silicon, and Google Connectomics pretraining systems experience. Leslie Valiant as academic advisor attracts downstream research talent into our orbit rather than theirs.

Historically, the large labs have acquired rather than built specialized capability, Google's DeepMind acquisition, Nvidia's Mellanox, Intel's Mobileye. This sector will be no different.

“This belongs in academia, not a startup.”

Every piece of industrial optimization software shipping today descended from academic research but was built outside the academy. CUDA came from Nvidia, not Stanford. Gurobi, the dominant commercial linear and integer programming solver, with revenue approaching $1B, was commercialized by engineers who left academia for exactly this reason. IBM's CPLEX, FICO's Xpress, Mosek: the same story.

Academic groups publish algorithms; they do not build industrial-scale developer ecosystems, customer-facing toolchains, benchmark suites, or tightly integrated commercial support. Universities do not optimize for integration; their incentive structures favour publication. The value in this space, and the gap, is productizing mathematical breakthroughs at scale. A startup is the correct vehicle, and Echea is structured explicitly to operate at the seam between the academic frontier and industrial deployment.

“Heuristic solvers are good enough.”

"Good enough" in this sector is a margin measured in billions of dollars per year. Every industry using heuristic optimization is paying a measurable optimality tax:

In EDA, current heuristic placement and routing tools leave 5–15% silicon area, wire length, and power on the table versus a hypothetical optimum. On a flagship TSMC 3nm tape-out costing $300M+, a 3% area improvement is $9M+ per chip family, and a fab ships many families per year.
In quant trading, heuristic order-scheduling loses tens of basis points of alpha per year at tier-1 firms , hundreds of millions in absolute terms at a $100B AUM shop. It also cannot produce the deterministic proof trails that regulators increasingly require.
In logistics and manufacturing scheduling, heuristic operations-research software (the core of the Gurobi/CPLEX market) is priced at low six figures per seat precisely because small percentage improvements in schedule quality translate into meaningful top-line gains.
In drug design, combinatorial search over chemical space is constrained by heuristic methods; enlarging the searchable region by even an order of magnitude materially increases hit rates in lead discovery.

"Good enough" is the marketing of the current incumbents. Every point of that optimality tax is a revenue opportunity for better solvers.

“#P-complete problems are decades old and nobody has cracked them. Why would you?”

Historically, every meaningful breakthrough on a #P-complete problem has come from one narrow mathematical object: the determinant and its surprising algebraic generalizations. The determinant is the canonical example of a polynomial-time-computable function that unexpectedly captures rich combinatorial counting structure, and its generalizations have been responsible for essentially all of the field's celebrated positive results.

Consider the precedent. The matrix-tree theorem (Kirchhoff, 1847) reduces counting spanning trees of a graph, a combinatorial object, to the determinant of the Laplacian matrix, giving a polynomial-time algorithm for a problem that looks exponential on its face. The FKT algorithm (Fisher, Kasteleyn, Temperley) solves counting perfect matchings in planar graphs, which is #P-complete in the general case, in polynomial time, using the Pfaffian (a determinant-like object). Holographic algorithms (Valiant, 2004) generalize this further: entire families of #P-complete problems collapse to polynomial time when the problem's structure admits an encoding into matchgates and Pfaffians. Holant problems and matchgate tractability extend the framework still further.

The pattern is consistent: the surprising positive results in #P-complete counting have always come from determinants, Pfaffians, and their algebraic generalizations. And those generalizations continue to appear. Recent work on spectral characterizations of graph polynomials, algebraic and topological invariants from cohomology applied to constraint satisfaction, and deep connections between #SAT, permanents, and tensor decompositions are actively opening new structural hooks into the #P-complete landscape.

Our team includes Leslie Valiant, the Turing laureate who defined the #P complexity class, proved the #P-completeness of the permanent, and invented holographic algorithms. That is not a coincidence. The intellectual lineage Echea is pursuing is precisely the lineage that has produced every prior breakthrough in this field, and that lineage is still actively generalizing. The existing body of work on determinants and their extensions is not a dead end, it is the most productive research programme in computational complexity, and the next generalization is the most natural place to look for the next breakthrough.

“Sales cycles in EDA and finance are long.”

Long sales cycles are real. EDA procurement runs 9–18 months; finance procurement runs 6–12 months. The business is structured to absorb them.

The founder network is already engaged with tier-1 targets through Etched, prior Harvard and Google relationships, and Leslie Valiant's academic network. Warm introductions exist today.

Pilots are priced asymmetrically against downstream economic value, not against cost: a single-digit-million pilot is trivial versus the hundreds of millions at stake per chip tape-out, and smaller still versus the alpha at stake in high-frequency trading infrastructure. Palantir, SpaceX, and Anduril all overcame worse cycles in even more conservative industries (defense, aerospace, government) through direct technical engagement, reference customers, and founder-led sales. Echea is structured similarly.

In parallel, the research publication track, first paper shipped, second in progress, is designed to generate pull from adjacent industries. Academic and industrial researchers will bring the technology to their employers as citations and benchmark results accumulate.

Risks & Mitigations

Research risk on the upside case. The 10,000× path depends on breakthroughs in applying algebraic and topological methods to #SAT at scale. Mitigation: the 10× path is not contingent on these breakthroughs, and generates revenue on its own.
Sales cycle length in EDA and quant trading is long. Mitigation: founder networks already engaged with beachhead targets; pilots can be priced asymmetrically against the headline economic value of even single-digit-percent area or alpha improvements.
Talent density. The intersection of deep SAT expertise and CUDA-level systems engineering is rare. Mitigation: the team's Harvard / MIT / Stanford / Etched / Google network covers both sides, and Leslie Valiant's mentorship materially expands recruiting reach.

Appendix

The Counting Connection

Every SAT problem has a counting twin. SAT asks does a solution exist? #SAT asks how many? Counting subsumes deciding.

Modern SAT solvers are built on heuristics, the same way ML is. #SAT is different: it admits real mathematics, algebraic graph theory, spectral methods, algebraic topology, which heuristics cannot reach. That is the source of the breakthroughs.

Echea

Formal Reasoning for Superintelligence

Formal Reasoning: No Guessing

One Problem Class. Every Industry.

One Math. Every Industry.

SAT Scaling Laws

Self Recursive Intelligence

Beyond Gradient Descent

Darts in the Dark

The Middle Ground

Math Trains the Machine

Pre-Training Reversed

Name the Destination

Chips Perfected

The Silicon Puzzle, Solved

Research & Theory

The Work, In Public

Counting Vertex Covers

The Year Ahead