Hey Michael,

To follow up on what John Baez said:

> You would need some feedback, and practice to learn how to write up proofs the way mathematicians do. This is math grad students spend so much time doing homeworks full of proofs, and I spend so much time grading these, writing comments in the margin, and showing all the students the 'best' proofs, so they can learn what good examples are like.

I've seen some free MOOCs where students grade one another. In this forum, I know I make my fair share of mistakes. Other students kindly point them out, so I have had a lot of chance to improve.

John gave you a head start on the proof of the puzzle:

> Assume \\(f : X \to Y\\) is monotone and define \\(\Phi\\) by

>

> \[ \Phi(x,y) \text{ if and only if } f(x) \le y .\]

>

> We want to prove \\(\Phi\\) is a feasibility relation. So, it suffices to show

>

> 1. If \\(\Phi(x,y) = \text{true}\\) and \\(x' \le x\\) then \\(\Phi(x',y) = \text{true}\\).

> 2. If \\(\Phi(x,y) = \text{true}\\) and \\(y \le y'\\) then \\(\Phi(x,y') = \text{true}\\).

Sadly, you can't just show

$$\Phi(x',y') = \text{true}$$

You have to show (1) and (2).

So let's prove (1).

**Proof**. Assume (a) \\(\Phi(x,y) = \text{true}\\) and (b) \\(x' \le x\\). We must show \\(\Phi(x',y) = \text{true}\\).

From (a), we know since \\(\Phi(x,y) \text{ if and only if } f(x) \le y\\) that:

\[ f(x) \leq y \tag{c}\]

By (b) and the assumption that \\(f\\) is monotone, we have

\[f(x') \le f(x) \tag{d}\]

From (c) and (d) we have by the transitivity of the preorder relation \\(\leq\\)

\[f(x') \le y \]

This, along with \\(\Phi(x,y) \text{ if and only if } f(x) \le y\\), suffices to show \\(\Phi(x',y) = \text{true}\\) as desired.

----------------------------------

There are many styles of proof.

TLA+ is a computer proof system. It has been used to analyze software systems at Amazon looking for bugs. The author of TLA+, Leslie Lamport, has some opinions about how proofs should be written. You can read them in [*How to Write a 21st Century Proof*](https://lamport.azurewebsites.net/pubs/proof.pdf).

I have done a lot of computer proofs. They are in my opinion, mechanical and boring. But, you can get really good at writing technically correct proofs, since you have the computer to check you.

But I think proofs are like artwork. If you want to read *beautiful* proofs, I recommend [*Proofs from THE BOOK* (2013)](https://www.amazon.com/Proofs-BOOK-Martin-Aigner/dp/3642008550) by Aigner, Ziegler and Hofmann.

I suspect John Baez feels the same, perhaps he will stop by and make some reading suggestions...

To follow up on what John Baez said:

> You would need some feedback, and practice to learn how to write up proofs the way mathematicians do. This is math grad students spend so much time doing homeworks full of proofs, and I spend so much time grading these, writing comments in the margin, and showing all the students the 'best' proofs, so they can learn what good examples are like.

I've seen some free MOOCs where students grade one another. In this forum, I know I make my fair share of mistakes. Other students kindly point them out, so I have had a lot of chance to improve.

John gave you a head start on the proof of the puzzle:

> Assume \\(f : X \to Y\\) is monotone and define \\(\Phi\\) by

>

> \[ \Phi(x,y) \text{ if and only if } f(x) \le y .\]

>

> We want to prove \\(\Phi\\) is a feasibility relation. So, it suffices to show

>

> 1. If \\(\Phi(x,y) = \text{true}\\) and \\(x' \le x\\) then \\(\Phi(x',y) = \text{true}\\).

> 2. If \\(\Phi(x,y) = \text{true}\\) and \\(y \le y'\\) then \\(\Phi(x,y') = \text{true}\\).

Sadly, you can't just show

$$\Phi(x',y') = \text{true}$$

You have to show (1) and (2).

So let's prove (1).

**Proof**. Assume (a) \\(\Phi(x,y) = \text{true}\\) and (b) \\(x' \le x\\). We must show \\(\Phi(x',y) = \text{true}\\).

From (a), we know since \\(\Phi(x,y) \text{ if and only if } f(x) \le y\\) that:

\[ f(x) \leq y \tag{c}\]

By (b) and the assumption that \\(f\\) is monotone, we have

\[f(x') \le f(x) \tag{d}\]

From (c) and (d) we have by the transitivity of the preorder relation \\(\leq\\)

\[f(x') \le y \]

This, along with \\(\Phi(x,y) \text{ if and only if } f(x) \le y\\), suffices to show \\(\Phi(x',y) = \text{true}\\) as desired.

----------------------------------

There are many styles of proof.

TLA+ is a computer proof system. It has been used to analyze software systems at Amazon looking for bugs. The author of TLA+, Leslie Lamport, has some opinions about how proofs should be written. You can read them in [*How to Write a 21st Century Proof*](https://lamport.azurewebsites.net/pubs/proof.pdf).

I have done a lot of computer proofs. They are in my opinion, mechanical and boring. But, you can get really good at writing technically correct proofs, since you have the computer to check you.

But I think proofs are like artwork. If you want to read *beautiful* proofs, I recommend [*Proofs from THE BOOK* (2013)](https://www.amazon.com/Proofs-BOOK-Martin-Aigner/dp/3642008550) by Aigner, Ziegler and Hofmann.

I suspect John Baez feels the same, perhaps he will stop by and make some reading suggestions...