The original motivation for creating Lean was software verification

"The main motivation, the original motivation for (creating) Lean was in software verification, right? I mean, Z3 was very popular at bug finding, for bug finding at Microsoft, was very influential there. But (for) Lean the goal was, can we make the same, have the same success of software verification? We went to a very strange path. I mean, having impact in mathematics that we never dreamt of. But the goal in both cases is like we, both in software mathematics and in AI, today rely on manual review, partial testing. A mistake in a theorem can be catastrophic, invalidating the whole result. The same thing (happens) for a critical piece of software, right? And one thing I see all the time, people fearing to make a change a piece of software because they fear by making the change they may be introducing a bug, especially if it's a critical piece of software." Watch more in the video below and in the full talk at the following link: From "Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI"

May 18, 2025 - 15:24

The original motivation for creating Lean was software verification

"The main motivation, the original motivation for (creating) Lean was in software verification, right? I mean, Z3 was very popular at bug finding, for bug finding at Microsoft, was very influential there. But (for) Lean the goal was, can we make the same, have the same success of software verification?

We went to a very strange path. I mean, having impact in mathematics that we never dreamt of.

But the goal in both cases is like we, both in software mathematics and in AI, today rely on manual review, partial testing. A mistake in a theorem can be catastrophic, invalidating the whole result. The same thing (happens) for a critical piece of software, right? And one thing I see all the time, people fearing to make a change a piece of software because they fear by making the change they may be introducing a bug, especially if it's a critical piece of software."

Watch more in the video below and in the full talk at the following link:

From "Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI"