contribute to a groundbreaking mathematical AI project

Stream: mathlib4

[Edouard d'Archimbaud]

We’re looking for talented individuals proficient in Lean 4/mathlib to contribute to an ambitious LLM project aimed at creating a mathematical superintelligence.

The project is open source and open data, but the role itself is paid.

Our goal is to accelerate progress in quantitative fields, including science and engineering, by leveraging LLMs capable of advanced mathematical reasoning.

Would you be interested in exploring this opportunity or discussing it further? If you know anyone who might be a good fit, I’d appreciate your recommendations.

Here’s more detail on the project and your potential contribution:

Modern AI systems based on large language models have shown remarkable language processing abilities, mimicking human-like understanding. However, they fall short in reasoning, often producing inaccurate outputs with high confidence—leading to unpredictable failures. These limitations make them unsuitable for critical applications where reliability is key.
In contrast, models capable of formal mathematical reasoning can guarantee correct outputs with transparent, interpretable reasoning steps. We believe this approach will make AI fundamentally safer, offering robust applications in fields like aerospace, chip design, industrial systems, and healthcare.

Our vision is to build a model that can automatically translate natural language math problems into their formal representations in Lean 4—and this is where your expertise comes in.

The role is paid, and even a few hours a day of contribution would be incredibly valuable.

And again, all project results (code, data) will be open source.

Looking forward to hearing from you!