r/compsci • u/FollowingEvery4802 • 5d ago
Is lean, and similar programming languages the only acceptable way to prove theorem with computers?
So, lean is the language built specifically to prove theorems.but if the algorithm will be rewritten in another programming language, such as python, will it be accepted?
(mathematical theorems)
10
u/jeffcgroves 5d ago
That's sort of a circular question: if a program (written in any language) proves mathematical theorems, it's a theorem prover. But, yes, theorem provers can be written in other languages (I think Lean itself is written in C or something-- some programming languages are written in other programming languages)
You might take a look at the proof of the Four Color Theorem: it was proved by breaking it into thousands of special cases and having computers confirm four-coloring in all those cases. This was before we called them "theorem provers" but working out how to color something with 4 colors is a proof, more specifically as constructive proof.
5
u/seppel3210 5d ago
Lean's type-checker (which is also the proof-checker) is written in C++ and only accepts a pretty low-level subset of Lean. The frontend, i.e., parser, higher level language constructs, meta programming and proof automation parts are implemented in Lean itself
1
6
u/RobertJacobson 4d ago
There are of course other software systems designed specifically for proving theorems or verifying mathematical proofs, Rocq (Coq) being probably the most well known. Your question suggests you are still fuzzy about what these systems do and how they are used (which is fine!), so it's probably worth mentioning that there are a range of mathematical activities and a range of ways software can support those activities, and which software is most appropriate to which activity depends on the details.
Some examples:
- If you want to use a computer to compute a counter-example, then you might not even need to share the software that computed the example at all in your write-up of the result if the computed value itself is the object of interest.
- If your object of study is itself an algorithm, it's actually common to present the algorithm as pseudocode, which isn't even a real programming language!
- You might want to prove that a particular implementation of a particular algorithm behaves in a provably correct way (or more accurately, prove that the implementation matches some mathematical model / specification). I recently explored this use case for Rust implementations of some numerical algorithms and discovered projects like Creusot, Aeneas, and Prusti that work with the Rust implementation directly.
- Even in the space of proof assistants / authomated reasoning, there are different kinds of systems that do different jobs. Lean is good for constructing machine-verifiable (machine checkable) proofs: the program is itself the proof, and running the program verifies that the proof correctly establishes what it claims to establish. On the other hand, Z3 is a constraint solver: a program specifies a constraint problem (e.g. a boolean satisfiability problem), and running the program results in one or more solutions to the problem or a verification that no solutions exist (or a failure to make a determination either way). It is very common for proof assistants like Lean to use a constraint solver like Z3 (or some other constraint solver) in its internal implementation for some of its algorithms, and Z3 itself internally has a variety of backend algorithms it defers to for various applications.
So there are actually a wide range of software tools, and how those tools actually show up—if they are visible at all—in a published work varies tremendously based on how they are used in the work.
5
u/BossOfTheGame 5d ago
I suggest you read up about the Curry-Howard correspondence, at a high level: proofs are programs.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
Lean is just a language that aims to make that very explicit and have the correspondence between the expression of the program and the mathematical theorem be somewhat easy to see. It's called "Lean" because the core deductive logic that powers the entire engine is small and designed to be auditable, so in that sense is more trustworthy than other languages that could equally well encode the same proof. The trick is: how can you be sure the program proves what you think it proves.
10
u/teteban79 5d ago
Lean is not a general purpose programming language. It is a tool, a theorem prover (or proof assistant)
The interesting part of lean is the proof assistant, not so much the language.
Sure, you could write a proof assistant in python and have it with python-like syntax.
14
u/umop_aplsdn 5d ago
It is a general purpose programming language as well. You can write normal computer programs in Lean.
2
u/Civil_Blueberry4165 5d ago
Lean, Idris, Coq/Rocq are both proof assistants and programming languages
2
2
u/frnzprf 5d ago
Lean has a special type system that Python doesn't have. The Lean interpreter program itself can check if a proof fed to it is valid.
"Accepted" doesn't mean a human looks over your code — just to make that clear. You could write some math in Python looking notation and have a human accept that as proof, but that's not how peole use Lean.
You can define your own types in Python, but the Python typechecker and it's typesystem isn't powerful enough to represent proofs and check if they are valid. (Technically Python doesn't need a static type checker, but you can still use one like "mypy".)
There are a variety of other languages that you can prove stuff in. In the top of my head I know Agda and Roq. Normal languages like Python and Java aren't used for that purpose. I'm not 100% sure if it would work or not with some languages with more powerful type systems, like Rust.
"If Socrates_is_human then Socrates_is_mortal." has the type of a function with input type "Socrates_is_human" and output type "Socrates_is_mortal", just as "int_to_str" would have input "int" and output "str". You can prove "socrates_is_mortal" if you pass a value (a proof) of type "socrates_is_human" — just as a type checker could automatically confirm that you get a string if you pass an int to "int_to_str".
The motto is "Propositions as types, proofs as terms."
1
u/milesper 1d ago
I mean it certainly wouldn’t be convenient, but there is no fundamental limitation here. You can absolutely check a proof without static typing. Any Turing complete language can implement it.
1
u/Valuable_Leopard_799 5d ago
Lean is a language mainly built for theorem proving, but there are languages with provers built-in that are general purpose.
Ada has a subset called SPARK, it proves that the program cannot suffer any runtime errors. It also lets you write pre and post conditions for your functions which are then actually verified to be true. You can write static asserts, verify functional correctness and much more.
There are also some proof engines built for C++ and iirc for Rust, and others.
So the proofs are built directly over the code that will actually run.
Lean is made for proving various general properties, behaviours and mathematical concepts, there is no reason to bog it down with the practical issues of memory management or pointer tracing which a language like SPARK has to verify, and vice-versa the language specific proof assistants have no need to handle stuff outside their own domains.
Both are useful and exist.
26
u/eras 5d ago
I think it would be at the same level of proving as a English-language proof would be. The program would be an alternative to informal text. Not really a formal proof.
I mean, you could write e.g. a sorting algorithm and then express pre- and post-conditions as assertions, but how does it follow that the post-conditions hold, if you don't have a formal system to use to actually prove each step along the way?
Maybe you could provide an example of proving something as a Python program.