The personal AI proof engineer

Stream: Machine Learning for Theorem Proving

[Jesse Michael Han]

Today, we announced our plans to build the personal AI proof engineer for Lean, in partnership with the Lean FRO.

https://morph.so/blog/the-personal-ai-proof-engineer/

The personal AI proof engineer will know mathlib and the relevant mathematical literature better than you 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.

We also open-sourced the weights for Morph Prover v0 7B today. We hope that this spurs further work by the community on conversational assistants for autoformalization. This was the result of a collaboration with @Brando Miranda, the STAIR group at Stanford, and Nous Research. It achieves a new state of the art for autoformalization while performing better than the original Mistral model on benchmarks like AGIEval and MMLU. The proving assistants that we will soon release will represent far more advanced versions of this model. A free hosted version for interactive use will be available soon.

https://huggingface.co/morph-labs/morph-prover-v0-7b

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.

We are hiring for research and engineering positions. If you believe, as we do, that the future of mathematics is inextricably linked to the future of software engineering, find me jesse@morph.so.

[Chris Hughes]

You might want to post this in job postings