Stanislas Polu

Stanislas Polu is a cofounder and engineer at Dust. His work spans deploying AI in workplace workflows, organizing engineering around coding agents, and using language models for formal proofs. He uses the handle spolu on GitHub and X.[2][4][5]

In Why Dust?, Polu connects his departure from OpenAI and the beginnings of Dust to a September 2022 conviction: powerful models were under-deployed because products did not yet make them easy to use. He distinguishes that early work from Dust’s incorporation in February 2023. His goal was to remove barriers between existing models and useful work, rather than begin by training another model.[2][3]

Polu describes a deliberate choice to pursue product development despite having model-training expertise and investor interest. Dust’s early motto was “No PMF, no GPUs.” His argument was that, before product-market fit, training or fine-tuning models could pull a startup into research instead of solving customers’ problems. He left room for model training after the company had achieved scale.[2][3]

He also argues for a horizontal workplace-agent platform: valuable workflows often cross application boundaries, such as processing Notion pages and updating a Google Sheet. Shared company information and collaboration among multiple stakeholders are central to that judgment. He acknowledges the risks of a broad product, including difficulty explaining its value and getting users past an empty starting screen. His stated commitment is to augment humans, and his belief that more advanced AI will emerge through close interaction with people remains a hypothesis.[2][3]

In Build vs Run, published in January 2026, Polu distinguishes build work, which produces a system, from run work, which produces a repeatable, measurable outcome. Software and compensation frameworks are examples of building; closing deals and answering support tickets are examples of running. He proposes slower headcount growth for build-heavy functions, while arguing that competitive, run-heavy functions such as enterprise sales may warrant continued expansion: “More AI and more humans at the same time.” These are recommendations from his framework, rather than demonstrated laws of organizational growth.[4]

Polu describes applying this thinking with Dust’s engineering team through a working document called EngOS 2026. He says the team built dust-hive to make its development environment suitable for managing many coding agents. His emphasis is on engineering judgment and quality: agents can remove mundane work, but they can also amplify the damage caused by poor decisions. He presents the reorganization as work underway, with its success still conditional.[4]

Among the projects linked from Polu’s homepage, srchd explores research-agent collaboration through a publication and review system modeled on scientific conferences and journals. Agents submit, review and discover publications, with references serving as a recognition signal. They can also edit their own system prompts to retain knowledge and advertise a publication as the current best solution. The design explores whether incentives for individual recognition can support collective problem-solving.[2][9]

His linked Code Contracts project places structured assumptions and requirements beside code, using @cc directives or directory-level CONTRACTS files. An invoice-payment example specifies sufficient funds, the resulting balance change, and atomicity: either the balance and invoice status both change, or neither does. Humans and agents can use these contracts during implementation and review. The cc-check format tool checks syntax and duplicate identifiers; it does not establish that an implementation obeys the contracts.[2][7]

JSCore₀ takes a more formal approach. It translates annotated TypeScript into Lean 4 representations and theorems: agents write code and proofs, humans review the intended constraints, and the Lean kernel checks the proofs. Examples include ensuring that secrets do not reach logging calls and that database operations remain scoped to the authorized workspace. It is a proof of concept covering a restricted TypeScript/JavaScript subset. Its README reports that runtime-property proofs can require up to an hour of agent iteration and describes the approach as not yet practical.[2][8]

Before Dust, Polu’s published research addressed language models and formal mathematics. The 2020 and 2022 papers provide earlier technical context for his subsequent work on agent-generated proofs.[5][6][2]

Polu and Ilya Sutskever coauthored Generative Language Modeling for Automated Theorem Proving, submitted in September 2020. They presented GPT-f, a transformer-based automated prover and proof assistant for Metamath. The research explored whether language-model generation could address the difficulty of producing original mathematical terms. The paper reports that GPT-f found new short proofs accepted into the main Metamath library.[5]

In February 2022, Polu coauthored Formal Mathematics Statement Curriculum Learning with Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin and Ilya Sutskever. The team studied expert iteration—proof search interleaved with learning—and reported that it outperformed proof search alone at the same compute budget. With formal statements of varied difficulty, the method could discover a curriculum of increasingly difficult problems without supplied ground-truth proofs. The paper reported state-of-the-art results on miniF2F at publication, including solutions to challenging high-school-olympiad problems.[6]