# Jokes

#### paulmdrdo

##### Active member
I have discovered a small error in your proof: since it leads to a contradiction, you must have divided by zero. The correct conclusion should be:

no = -1.
it's a joke anyway. #### Deveno

##### Well-known member
MHB Math Scholar
it's a joke anyway. Indeed, I realize that. And, see, my reply is a joke, too, because I am responding as if a "joke" were "serious math" which is sheer lunacy. #### Evgeny.Makarov

##### Well-known member
MHB Math Scholar
it's a joke anyway. Be it as it may, a large portion of the "proof" actually makes sense.

\begin{aligned} \text{study} &= \text{no fail}\\ \text{no study} &= \phantom{no }\,\text{fail}\end{aligned}
If we add these two expressions together, we see that
$\text{study}+\text{no study} = \text{no fail}+\text{fail}$
This implies that
$(1+\text{no})\text{study} = (1+\text{no})\text{fail}$
Cancelling out the common term now leaves us with
$\text{study} = \text{fail}$
Here is a code for the Coq proof assistant.

Code:
Variables study fail : Prop.

Hypothesis h1 : study <-> ~fail.
Hypothesis h2 : ~study <-> fail.

Lemma l1 : study \/ ~study <-> fail \/ ~fail.
Proof. rewrite h2, h1; tauto. Qed.

Definition prop2_plus (f1 f2 : Prop -> Prop) (P : Prop) :=
f1 P \/ f2 P.

Infix "+" := prop2_plus.

Lemma l2 : (id + not) study <-> (id + not) fail.
Proof. apply l1. Qed.
Here Prop is the type of propositions, i.e., the type of Boolean formulas. Disjunction is denoted by \/ and the negation not is denoted by ~.

The formulas (study \/ ~study) and (fail \/ ~fail) have the same shape, so the idea is to factor out this shape. A similar thing can be done with numbers. The expressions $2+3\cdot2^2$ and $5+8\cdot5^2$ look similar. We can define a function $f(x,y)=x+yx^2$ and represent the two expressions as $f(2,3)$ and $f(5,8)$, respectively. In the same way, we define a function that takes and returns propositions: $f(P)=P\lor{\sim}P$, and say that $f(\text{study})\leftrightarrow f(\text{fail})$.

To make it even more similar to (1 + no)study = (1 + no) = fail from the original proof, we define a higher-order function prop2_plus that takes two functions of type (Prop -> Prop) and returns a similar function. It is basically a pointwise disjunction. It is needed because we cannot apply regular disjunction, which has type Prop -> Prop -> Prop, to the identity function id and the negation not : Prop -> Prop. And voilà,

(id + not) study <-> (id + not) fail.

The only thing is that this is not multiplication, but function application. And since (id + not) is not injective, unlike multiplication by a nonnegative number, we cannot conclude that study <-> fail.

This ability to define functions not only on datatypes like numbers and strings, but also on propositions, as well as the ability to define higher-order functions (those that take functions as arguments) are characteristics of the so called type theory, on which Coq is based.

OK, I'll crawl back into my nerdy hovel now...

#### topsquark

##### Well-known member
MHB Math Helper
Be it as it may, a large portion of the "proof" actually makes sense.

Here is a code for the Coq proof assistant.

Code:
Variables study fail : Prop.

Hypothesis h1 : study <-> ~fail.
Hypothesis h2 : ~study <-> fail.

Lemma l1 : study \/ ~study <-> fail \/ ~fail.
Proof. rewrite h2, h1; tauto. Qed.

Definition prop2_plus (f1 f2 : Prop -> Prop) (P : Prop) :=
f1 P \/ f2 P.

Infix "+" := prop2_plus.

Lemma l2 : (id + not) study <-> (id + not) fail.
Proof. apply l1. Qed.
Here Prop is the type of propositions, i.e., the type of Boolean formulas. Disjunction is denoted by \/ and the negation not is denoted by ~.

The formulas (study \/ ~study) and (fail \/ ~fail) have the same shape, so the idea is to factor out this shape. A similar thing can be done with numbers. The expressions $2+3\cdot2^2$ and $5+8\cdot5^2$ look similar. We can define a function $f(x,y)=x+yx^2$ and represent the two expressions as $f(2,3)$ and $f(5,8)$, respectively. In the same way, we define a function that takes and returns propositions: $f(P)=P\lor{\sim}P$, and say that $f(\text{study})\leftrightarrow f(\text{fail})$.

To make it even more similar to (1 + no)study = (1 + no) = fail from the original proof, we define a higher-order function prop2_plus that takes two functions of type (Prop -> Prop) and returns a similar function. It is basically a pointwise disjunction. It is needed because we cannot apply regular disjunction, which has type Prop -> Prop -> Prop, to the identity function id and the negation not : Prop -> Prop. And voilà,

(id + not) study <-> (id + not) fail.

The only thing is that this is not multiplication, but function application. And since (id + not) is not injective, unlike multiplication by a nonnegative number, we cannot conclude that study <-> fail.

This ability to define functions not only on datatypes like numbers and strings, but also on propositions, as well as the ability to define higher-order functions (those that take functions as arguments) are characteristics of the so called type theory, on which Coq is based.

OK, I'll crawl back into my nerdy hovel now...
I think I watched a Dr. Who episode based on this.

-Dan

#### anemone

##### MHB POTW Director
Staff member
1. Where was the Declaration of Independence signed?
Answer: On the bottom of the page.

2. River Ravi, flows in which state?
Answer: Liquid State.

3. What can you never eat for breakfast?
Answer: Lunch and Dinner

4. What looks like half an apple?
Answer: The other half.

5. What is the main reason for divorce?
Answer: Marriage

6. In which battle did Napoleon die?
Answer: His last one.

#### eddybob123

##### Active member
An infinite crowd of mathematicians enters a bar.
The first one orders a pint, the second one a half pint, the third one a quarter pint...
"I understand", says the bartender - and pours two pints.

#### agentmulder

##### Active member
An infinite crowd of mathematicians enters a bar.
The first one orders a pint, the second one a half pint, the third one a quarter pint...
"I understand", says the bartender - and pours two pints.
So the Hilbert Hotel also has a Hilbert Bar and Hilbert himself is tending bar with Cantor as the 'BOUNCER' #### Chris L T521

##### Well-known member
Staff member
Here are a couple jokes I came across recently! XD

[HR][/HR]
A Statistician, Engineer and Physicist go to the horse track. Each have their system for betting on the winner and they're sure of it.

After the race is over, the Statistician wanders into the nearby bar, defeated. He notices the Engineer, sits down next to him, and begins lamenting: "I don't understand it. I tabulated the recent performance of all these horses, cross-referenced them with trends for others of their breed, considered seasonal variability, everything. I couldn't have lost."

"Yeah," says the Engineer, "well, forget that. I ran simulations based on their weight, mechanical ratios, performance models, everything, and I'm no better off."

Suddenly, they notice a commotion in the corner. The Physicist is sitting there, buying rounds and counting his winnings. The Engineer and Statistician decide they've got to know, so they shuffle over and ask him, "what's your secret, how'd you do it?"

The Physicist leans back, takes a deep breath, and begins, "Well, first I assumed all the horses were spherical and identical..."

[HR][/HR]
A mathematician, a physicist, and an engineer are given the task of finding how high a particular red rubber ball will bounce when dropped from a given height onto a given surface.

The mathematician derives the elasticity of the ball from its chemical makeup, derives the equations to determine how high it will bounce and calculates it.

The physicist takes the ball into the lab, measures its elasticity, and plugs the variables into a formula.

The engineer looks it up in his red rubber ball book.

#### Chris L T521

##### Well-known member
Staff member
And one more (as a picture, though)! #### Deveno

##### Well-known member
MHB Math Scholar
Q: Why do mathematicians always make problems bigger?

A: Because of Cantor.

(Warning: Educated non-mathematicians may find this joke slightly funnier).

MHB Math Helper

#### eddybob123

##### Active member
Q: Why didn't Isaac Newton do group theory?
A: Because he wasn't Abel. BTW, if you already know some of the basics of group theory and want to get into more advanced material as well as applications, I recommend David Joyner's Adventures in Group Theory, published in 2002. It can't fail, because it has the above joke in it.

#### soroban

##### Well-known member

A reporter approaches a Saudi, a Hindu, a North Korean,
and a New Yorker.

He says, "Pardon me, what is your opinion on the beef shortage?"

The Saudi says, "What is a shortage?"

The Hindu says, "What is beef?"

The North Korean says, "What is an opinion?"

The New Yorker says, "What is pardon me?"

#### eddybob123

##### Active member
That was actually quite offensive. #### Bacterius

##### Well-known member
MHB Math Helper #### MarkFL

##### Administrator
Staff member
Well, it is safe to say that student's mind was not on mathematics that day! #### eddybob123

##### Active member
There are 10 types of people in the world: those who understand base 16, and F the rest. #### anemone

##### MHB POTW Director
Staff member MHB Math Helper

MHB Math Helper

#### Deveno

##### Well-known member
MHB Math Scholar
International Choice of Urinal Protocol...ohemgee!