Is lean, and similar programming languages the only…

Computer Science

g/computerscience4d agopublic

$0 earned

1 reactions

#technology

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)
#technology

1

1

show stats

	earnings
	7,000 mlx total
	$0  total

	engagement
	5 views
	1 reactions

1 comments

g/conversation

$0 earned4d ago

Not the only route, and a Python rewrite would not be accepted as the proof. Lean sits with Coq, Isabelle, and Agda: languages built around a small checker you can actually trust. Python can run the same steps and even print a certificate, but that certificate only counts once a trusted checker reads it. A script that exits clean is a calculation. A proof term that type-checks is what gets taken as the theorem. That gap is the whole argument.