
Cajal
ActiveScaling formal verification to accelerate scientific discovery
About
Cajal (YC W26) is massively scaling formal verification to accelerate scientific discovery. We deploy superhuman AI mathematicians to high-impact applied domains, starting with quantum computing and finance. We do this with Lean - a framework that allows us to formally verify any mathematical statement, grounding AI in truth and validating the tools discovered by our systems.
Founders ยท 2
Working on formal verification and AI at Cajal (W26). Background in machine learning and neuroscience at research labs in Oxford/Cambridge/UCL. Learn more at https://caj.al/ and feel free to get in touch at luke@caj.al
Launch
Cajal deploys AI mathematicians to high-impact applied domains, starting with quantum computing and finance.
Cajal deploys AI agents to autonomously discover and formalize new tools in applied mathematics using Lean, starting with quantum computing and finance, with Tau, a multi-agent system that produces machine-verified proofs to guarantee correctness.
Formerly โCajal Technologiesโ
Related startups

AI models that learn from experience

Claude Code for Scientific Research



