r/compsci • u/FollowingEvery4802 • 7d 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)

24 Upvotes

80% Upvoted

18 comments sorted by

View all comments

26

u/eras 7d 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.

13

u/Heavy-Difficulty6522 7d ago

I think the point is the curry-howard correspondence means that a proof IS a program, so any program or script is in effect a proof of some sort

5

u/CormacMacAleese 7d ago

ISTM that while every program might be a proof of some sort, it would follow that it's usually the proof of a theorem we didn't intend and can't state.

It reminds me of Dirk Gently scribbling on a bit of paper and saying, "I've just written the solution to the mystery--now we just need to answer the question: what language is this?"