4 ms·

Writing code and proving theories are flip sides of the same coin. See e.g. Phil Wadler’s “Proofs are Programs”: https://philarchive.org/rec/WADPAP https://phil

by antonvs 2mo ago

Writing code and proving theories are flip sides of the same coin. See e.g. Phil Wadler’s “Proofs are Programs”: https://philarchive.org/rec/WADPAP https://philarchive.org/rec/WADPAP The statement should probably really be “programs are proofs” since it’s difficult to make it a true bidirectional isomorphism, which is why the underlying principle is properly called the Curry-Howard(-Lambek) correspondence: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... The point is that the fact that LLMs are good at writing code directly implies that they should also be good at certain classes of mathematical proof.

inigyou 2mo ago
Not in any useful way, though. In the Curry-Howard correspondence, being able to write a function of type "int -> string" proves that there is at least one valid string or there are no valid ints. The code of the function is a proof of this statement. For example you might prove directly that there is a string, by writing return "hello"; or you might write return bool2string(int2bool(myInt)); thus chaining two implications to arrive at a shortcut implication.
- antonvs 2mo ago
  > Not in any useful way, though. Theorem provers and proof assistants like Lean, Coq/Rocq, Agda, Idris, NuPRL and Epigram all fundamentally depend on Curry-Howard. And again, the point is not that there’s some magical isomorphism, but that if LLMs are good at coding, they’re also likely to be good at certain classes of proof.
  - inigyou 2mo ago
    No they don't. They act on proofs, not on stupid conversions of proofs into useless programs.
    - antonvs 2mo ago
      You should take a look at "The Calculus of Constructions" (1988), which is one of the seminal papers that describes the basis for the Coq (now Rocq) theorem prover: https://www.academia.edu/47789825/The_calculus_of_constructions https://www.academia.edu/47789825/The_calculus_of_constructi... Here's a very relevant quote from the introduction: > "The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda-expression, typed with propositions of the underlying logic. By removing types we get a pure lambda-expression, expressing its associated algorithm. Computing this lambda-expression corresponds roughly to cut-elimination. It is our thesis that (as already advocated by Martin-L6f [36]) the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of a very high-level functional programming language, with complex polymorphism well-suited for module specification [8]. The notion of type encompasses the usual notion of data type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate." In other words, proofs are expressed as typed lambda terms, i.e. "proofs are programs". This is literally what such theorem provers are: examples of the Curry-Howard correspondence in action. If the correspondence didn't exist, none of these tools would exist. Here are a couple of quotes from one of the Lean papers, "Theorem Proving in Lean", https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf https://leanprover.github.io/theorem_proving_in_lean/theorem... : > "This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm." > "The match statement is part of Lean’s function definition system, which provides convenient and expressive ways of defining complex functions. Once again, it is the Curry-Howard isomorphism that allows us to co-opt this mechanism for writing proofs as well." All of the other theorem provers and proof assistants I mentioned rely on a similar approach.

by antonvs 2mo ago

inigyou 2mo ago

Not in any useful way, though. In the Curry-Howard correspondence, being able to write a function of type "int -> string" proves that there is at least one valid string or there are no valid ints. The code of the function is a proof of this statement. For example you might prove directly that there is a string, by writing return "hello"; or you might write return bool2string(int2bool(myInt)); thus chaining two implications to arrive at a shortcut implication.

antonvs 2mo ago
> Not in any useful way, though. Theorem provers and proof assistants like Lean, Coq/Rocq, Agda, Idris, NuPRL and Epigram all fundamentally depend on Curry-Howard. And again, the point is not that there’s some magical isomorphism, but that if LLMs are good at coding, they’re also likely to be good at certain classes of proof.
- inigyou 2mo ago
  No they don't. They act on proofs, not on stupid conversions of proofs into useless programs.
  - antonvs 2mo ago
    You should take a look at "The Calculus of Constructions" (1988), which is one of the seminal papers that describes the basis for the Coq (now Rocq) theorem prover: https://www.academia.edu/47789825/The_calculus_of_constructions https://www.academia.edu/47789825/The_calculus_of_constructi... Here's a very relevant quote from the introduction: > "The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda-expression, typed with propositions of the underlying logic. By removing types we get a pure lambda-expression, expressing its associated algorithm. Computing this lambda-expression corresponds roughly to cut-elimination. It is our thesis that (as already advocated by Martin-L6f [36]) the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of a very high-level functional programming language, with complex polymorphism well-suited for module specification [8]. The notion of type encompasses the usual notion of data type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate." In other words, proofs are expressed as typed lambda terms, i.e. "proofs are programs". This is literally what such theorem provers are: examples of the Curry-Howard correspondence in action. If the correspondence didn't exist, none of these tools would exist. Here are a couple of quotes from one of the Lean papers, "Theorem Proving in Lean", https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf https://leanprover.github.io/theorem_proving_in_lean/theorem... : > "This is the approach followed in the Calculus of Constructions, and hence in Lean as well. The fact that the rules for implication in a proof system for natural deduction correspond exactly to the rules governing abstraction and application for functions is an instance of the Curry-Howard isomorphism, sometimes known as the propositions-as-types paradigm." > "The match statement is part of Lean’s function definition system, which provides convenient and expressive ways of defining complex functions. Once again, it is the Curry-Howard isomorphism that allows us to co-opt this mechanism for writing proofs as well." All of the other theorem provers and proof assistants I mentioned rely on a similar approach.