__  
   ____ ___  ____  _________  / /_ 
  / __ `__ \/ __ \/ ___/ __ \/ __ \
 / / / / / / /_/ / /  / /_/ / / / /
/_/ /_/ /_/\____/_/  / .___/_/ /_/ 
                    /_/            
             
                

The personal AI proof engineer

At Morph Labs, our mission is to bring the personal AI software engineer to everyone. Today, we are coming out of stealth to announce we are working to solve computer-verified mathematics alongside the Lean programming language community and in partnership with the Lean FRO.

We are building the personal AI proof engineer to accelerate the formal mathematics revolution.

Solve math, solve programming

Hundreds of mathematicians have chosen to use Lean as the basis for mathlib, Lean's standard math library — what some call the mathematical library of the future.

The personal AI proof engineer will know mathlib and the relevant mathematical literature better than its human users do. It will be able to explain mathlib's APIs in natural language and make it 100x easier for novices to ramp up and become productive. It will stay up to date on the latest changes, PRs, branches, and forum discussions. It will be accessible from the web, mobile, and the IDE. Within the IDE, it will offer advice, suggest relevant lemmas, and automate proof search.

Lean is also a full-fledged programming language, and is one of the most advanced programming languages in the world. Lean makes it possible to simultaneously write a program and reason about its correctness with 100% confidence. Unit tests are merely an approximation to the specifications that Lean developers can guarantee around their programs. After we develop a compelling AI coding assistant for Lean, the same techniques can be applied to other languages and domains, and the resulting AIs will be better at reasoning about code as well.

Mathlib is rapidly approaching one million lines of code with dozens of new PRs merged every day. Some of the most interesting problems faced by mathlib developers belong to the domain of proof engineering sui generis and lie within the intersection of software engineering, software verification, and mathematics. It turns out, though, that many of the problems that arise when developing on top of a comprehensive computer-checkable mathematical library echo those faced by any software engineer working on top of a large-scale software monorepo. As such, Lean and its mathematical library are a rich testbed for AI developer tooling that already has far broader applications.

Morph Prover v0 7B

Today, we are releasing Morph Prover v0 7B, the first open-source model trained as a conversational assistant for Lean users. This model was trained in collaboration with Nous Research and the Stanford Trustworthy AI Research (STAIR) group led by professor Sanmi Koyejo, with major contributions by Brando Miranda and help from Peter Holderrieth of MIT and Jin Peng Zhou of Cornell. Morph Prover v0 7B is a chat fine-tune of Mistral trained on Zulip, Mathlib, GitHub, math textbook data, and Capybara. It achieves a new state of the art for autoformalization while performing better than the original Mistral model on benchmarks like AGIEval and MMLU. It was trained with our proprietary synthetic data pipeline using code data generated by the Morph Code Index.

The model can run at 20 tok/s on an M2 Macbook using llama.cpp, and thanks to our friends at Nomic AI, Morph Prover v0 7B can also run locally on any consumer GPU with GPT4All Vulkan support.

Access the model here.

While this is the best open-source model for Lean we have seen, this is an early research release which we hope to improve with feedback from the community. The proving assistants that we will soon release will represent far more advanced versions of this model. We are releasing Morph Prover v0 7B now in the hope that it stimulates further work on conversational assistants for autoformalization.

We intend to make long-term investments in AI developer tooling for Lean. User feedback will improve future versions of Morph Prover and other AI coding assistants for Lean in a virtuous cycle. We will soon begin work on the Lean AI Datalake, a centralized repository of human-AI feedback to be placed under the stewardship of the Lean FRO.

What's next

The future of mathematics is inextricably linked to the future of software engineering. We're optimistic about the future that we're building.

If you are too, reach us at jobs@morph.so.