Math Proof Generation

The Math Proof Generation (MPG) process creates mathematical proofs from the execution steps of a program.

MPG builds on this idea by automatically generating machine-checkable mathematical proofs from program executions.

This means that if a programming language has a formal definition in K, then any program run in that language can be turned into a mathematical proof. Importantly, this mathematical proof can be checked without relying on K or any other specific tools.

Below is a general outline of how a mathematical proof, represented as Proof, is created from a program, represented as Program, written in a language, represented as Lang:

1. The semantics of Lang, written in the K framework, are compiled into Kore format, becoming the Lang math theory.

2. K's LLVM execution engine takes the Lang math theory, the Prog, and any other necessary execution environment inputs to produce proof hints. These "hints" are essentially a record of the execution steps the program takes, based on the defined semantics of Lang.

3. The MPG process then uses these proof hints, the Lang math theory, and a set of predefined rules (from a proof calculus) to create an internal representation of the mathematical proof.

4. Finally, this internal representation is converted into a format that a proof checker can understand, such as Metamath or a specialized block model. This allows the proof to be verified by a machine, either directly or through a zkVM.

In essence, MPG transforms a program's execution into a mathematical proof that a machine can verify. This involves:

• Formally defining the language.

• Running the program and recording "hints" about its execution.

• Using these hints and a set of rules to construct the mathematical proof.

• Formatting the proof so a machine can check it.