The proof is trivial (variations on a theme)

The goal of this lecture note is to revisit Exercise 0 in Week 03, namely the generator of random mathematical proofs, and to analyze it in the manner of machine learning.

Resources

• The OCaml code for the present lecture note (latest version: 06 Feb 2020).

Situation

Here is a sample of random proofs, writing each of them on one line:

The proof is trivial!  Just view the problem as a continuous complexity class whose elements are exact monoids
The proof is trivial!  Just view the problem as an open DAG whose elements are skew-symmetric combinatorial games
The proof is trivial!  Just biject it to a non-degenerate topological space whose elements are dihedral rings
The proof is trivial!  Just biject it to a computable hypergraph whose elements are semi-decidable homeomorphisms
The proof is trivial!  Just view the problem as a structure-preserving ring whose elements are closed Cayley graphs

Observation

The phrasing of these proofs follows a clear pattern:

• they all start with “The proof is trivial! Just”,
• they all continue with either “view the problem as” or “biject it to”,
• they all continue with a technical term (e.g, “a continuous complexity class”),
• they all continue with “whose elements are”, and
• they all finish with another technical term (e.g., “exact monoids”).

Hypothesis

Let us formulate this phrasing as a grammar:

<proof> ::= "The proof is trivial!  Just " <verb> " " <complement1> " whose elements are " <complement2>

<verb> ::= "view the problem as" | "biject it to"

<complement1> ::= "a continuous complexity class"
                | "an open DAG"
                | "a non-degenerate topological space"
                | "a computable hypergraph"

<complement2> ::= "exact monoids"
                | "skew-symmetric combinatorial games"
                | "dihedral rings"
                | "semi-decidable homeomorphisms"
                | "closed Cayley graphs"

Experiment

We can verify that each of the proofs in the sample can be parsed according to this grammar.

We can also sample more proofs and both

• verify that the grammar captures the structure of the new proofs, and
• expand the grammar with more productions by adding new terminals for each of <complement1> and <complement2>.

Generating our own random proofs

Let us implement our own generator of random proofs, using OCaml’s generator of random integers to pick random terminals in the grammar.

For example, here is a generator of random verbs:

let make_verb () =
  if Random.int 2 = 0
  then "view the problem as"
  else "biject it to";;

Applying make_verb to the unit value randomly yields either of "view the problem as" and "biject it to":

# make_verb ();;
- : string = "view the problem as"
# make_verb ();;
- : string = "biject it to"
# make_verb ();;
- : string = "view the problem as"
#

Likewise for generating random complements:

let make_complement1 () =
  let n = Random.int 4
  in if n = 0
     then "a continuous complexity class"
     else if n = 1
     then "an open DAG"
     else if n = 2
     then "a non-degenerate topological space"
     else "a computable hypergraph";;

let make_complement2 () =
  let n = Random.int 5
  in if n = 0
     then "exact monoids"
     else if n = 1
     then "skew-symmetric combinatorial games"
     else if n = 2
     then "dihedral rings"
     else if n = 3
     then "semi-decidable homeomorphisms"
     else "closed Cayley graphs";;

And now we can generate random proofs by stringing together (using string concatenation) random verbs and random complements in the template of a proof:

let make_proof () =
  "The proof is trivial! Just " ^ make_verb () ^ " " ^ make_complement1 () ^ " whose elements are " ^ make_complement2 ();;

To wit:

# make_proof ();;
- : string =
"The proof is trivial! Just view the problem as a continuous complexity class whose elements are semi-decidable homeomorphisms"
# make_proof ();;
- : string =
"The proof is trivial! Just biject it to a continuous complexity class whose elements are closed Cayley graphs"
# make_proof ();;
- : string =
"The proof is trivial! Just biject it to an open DAG whose elements are skew-symmetric combinatorial games"
# make_proof ();;
- : string =
"The proof is trivial! Just biject it to a continuous complexity class whose elements are dihedral rings"
# make_proof ();;
- : string =
"The proof is trivial! Just biject it to a continuous complexity class whose elements are semi-decidable homeomorphisms"
# make_proof ();;
- : string =
"The proof is trivial! Just view the problem as a non-degenerate topological space whose elements are closed Cayley graphs"
#

Exercise 7

1. Sample more random proofs online and expand the grammar and the generator accordingly.
2. In English, sentences typically end with a period. Modify the proof generator so that the generated proofs also end with a period, like the two sentences composing the present paragraph.

Exercise 8

Revisit Strachey’s generator of love letters and implement your own.

Resources

• The OCaml code for the present lecture note (latest version: 06 Feb 2020).

Version

Created [06 Feb 2020]