Write it into number theory style

Question

Write a mathematical statement, using the symbols:

• There exists at least one non-negative integer (written as E, existential quantifier)
• All non-negative integers(written as A, universal quantifier)
• + (addition)
• * (multiplication)
• = (equality)
• >, < (comparison operators)
• &(and), |(or), !(not)
• (, ) (for grouping)
• variable names

which is equivalent to the statement

There exists a rational number a, such that π + e * a is rational.

(of course, \$\pi =3.1415...\$ is the mathematical constant equal to the circumference divided by the diameter of a circle, and \$e=2.7182...\$ is Euler's number)

You must prove that your statement is indeed equivalent to the statement above.

Obviously, the "shortest" way to go about this is to prove the statement true or false, and then answer with a trivially true or false statement, as all true statements are equivalent to one another, as are all false statements.

However, the given statement’s truth value is an unsolved problem in mathematics: we don't even know if \$\pi+e\$ is irrational! Therefore, barring groundbreaking mathematical research, the challenge is to find a "simple" equivalent statement, prove its equivalence, and describe it as briefly as possible.

Scoring

E A + * = > < & | and ! each add 1 to the score. ( and ) don't add anything to the score. Each variable name adds 1 to the score.

E.g. E x (A ba x+ba>x*(x+ba)) score 13 (E x A ba x + ba > x * x + ba)

Lowest score wins.

---

Note:

_{Disclaimer: This note was not written by the OP.}

• This is not a code-golf challenge. Answers are not required to contain code.
• This is similar to, but not, a proof-golf challenge, as you need to write a statement and prove it being equivalent to another statement.
• You are allowed to submit a trivially-true (e.g., for all x, x = x Ax x=x) or a trivially-false statement (e.g., for all x, x> x Ax x>x) if you can prove the statement above is true/false.
• You are allowed to use additional symbols (similar to lemma in proof-golf), but the score would be counted the same as you not using them.
  For example, if you define a => b to mean (!a) | b, each time you use => in your proof, your score increases by 2.

• Because constants are not listed in the allowed symbols, you must not use them.
  For example: The statement 1 > 0 can be written as

  
  Forall zero: ( zero + zero = zero ) =>
  Forall one: ( Forall x: x * one = x ) =>
  one> zero
  

  at the score of 23. (remember that => costs 2 per use).

Hints

• To use natural constants, you may do E0, 0+0=0 & E1, At 1*t=t & (so you don't need => which is more expansive); for numbers larger than 1, just add some 1's

• xnor: I like the concept here, but the statement is really hard to write and I'd be impressed by any solution no matter the score. I would have suggested using something simpler so more people participate.
• Luis Mendo: You require a mathematical statement which is equivalent to the given one. In which sense should they be equivalent? If I am correct, the given statement is a false one. So its equivalence with other statements is hard for me to grasp. For example, is it equivalent to There exists a rational number a, such that i + e * a is rational (where i is the imaginary unit)?
• l4m2: Current note just say You are allowed to submit a trivially-true (e.g., for all x, x = x Ax x=x) or a trivially-false statement (e.g., for all x, x > x Ax x>x) if you can prove the statement above is true/false.. The statement is now neither proved nor disproved, so I really don't mind if problem gets boring because such a problem is solved
• lynn: The question as written seemed to majorly bury the lede, and avoid explaining what’s really going on, so I wrote a little explanation in the notes (that the non-triviality of the challenge is hinged on the currently unknown truth value of the given statement).
• l4m2: I'd be impressed by any solution no matter the score. The score was only to make an aim for those who can solve this problem

Answer 1

671

E a (a+a>a*a & (E b (E c (E d (A e (A f (f<a | (E g (E h (E i ((A j ((!(j=(f+f+h)*(f+f+h)+h | j=(f+f+a+i)*(f+f+a+i)+i) | j+a<e & (E k ((A l (!(l>a & (E m k=l*m)) | (E m l=e*m))) & (E l (E m (m<k & g=(e*l+(j+a))*k+m)))))) & (A k (!(E l (l=(j+k)*(j+k)+k+a & l<e & (E m ((A n (!(n>a & (E o m=n*o)) | (E o n=e*o))) & (E n (E o (o<m & g=(e*n+l)*m+o))))))) | j<a+a & k=a | (E l (E m ((E n (n=(l+m)*(l+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & g=(e*p+n)*o+q))))))) & j=l+a+a & k=j*j*m))))))) & (E j (E k (E l ((E m (m=(k+l)*(k+l)+l & (E n (n=(f+m)*(f+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & j=(e*p+n)*o+q))))))))) & (A m (A n (A o (!(E p (p=(n+o)*(n+o)+o & (E q (q=(m+p)*(m+p)+p+a & q<e & (E r ((A s (!(s>a & (E t r=s*t)) | (E t s=e*t))) & (E s (E t (t<r & j=(e*s+q)*r+t))))))))) | m<a & n=a & o=f | (E p (E q (E r (!(E s (s=(q+r)*(q+r)+r & (E t (t=(p+s)*(p+s)+s+a & t<e & (E u ((A v (!(v>a & (E w u=v*w)) | (E w v=e*w))) & (E v (E w (w<u & j=(e*v+t)*u+w))))))))) | m=p+a & n=(f+a)*q & o=f*r)))))))) & (E m (m=b*(h*f)*l & (E n (n=b*(h*f+h)*l & (E o (o=c*(k*f)*i & (E p (p=c*(k*f+k)*i & (E q (q=d*i*l & (m+o<q & n+p>q | m<p+q & n>o+q | o<n+q & p>m+q))))))))))))))))))))))))))

How it works

First, multiply through by the purported common denominators of a and (π + e·a) to rewrite the condition as: there exist a, b, c ∈ N (not all zero) with a·π + b·e = c or a·π − b·e = c or −a·π + b·e = c. Three cases are necessary to deal with sign issues.

Then we’ll need to rewrite this to talk about π and e via rational approximations: for all rational approximations π0 < π < π1 and e0 < e < e1, we have a·π0 + b·e0 < c < a·π1 + b·e1 or a·π0 − b·e1 < c < a·π1 + b·e0 or −a·π1 + b·e0 < c < −a·π0 + b·e1. (Note that we now get the "not all zero" condition for free.)

Now for the hard part. How do we get these rational approximations? We want to use formulas like

2/1 · 2/3 · 4/3 · 4/5 ⋯ (2·k)/(2·k + 1) < π/2 < 2/1 · 2/3 · 4/3 · 4/5 ⋯ (2·k)/(2·k + 1) · (2·k + 2)/(2·k + 1),

((k + 1)/k)^k < e < ((k + 1)/k)^{k + 1},

but there’s no obvious way to write the iterative definitions of these products. So we build up a bit of machinery that I first described in this Quora post. Define:

divides(d, a) := ∃b, a = d·b,

powerOfPrime(a, p) := ∀b, ((b> 1 and divides(b, a)) ⇒ divides(p, b)),

which is satisfied iff a = 1, or p = 1, or p is prime and a is a power of it. Then

isDigit(a, s, p) := a < p and ∃b, (powerOfPrime(b, p) and ∃q r, (r < b and s = (p·q + a)·b + r))

is satisfied iff a = 0, or a is a digit of the base-p number s. This lets us represent any finite set using the digits of some base-p number. Now we can translate iterative computations by writing, roughly, there exists a set of intermediate states such that the final state is in the set, and every state in the set is either the initial state or follows in one step from some other state in the set.

Details are in the code below.

Generating code in Haskell

{-# LANGUAGE ImplicitParams, TypeFamilies, Rank2Types #-}
-- Define an embedded domain-specific language for propositions.
infixr 2 :|
infixr 3 :&
infix 4 :=
infix 4 :>
infix 4 :<
infixl 6 :+
infixl 7 :*
data Nat v
 = Var v
 | Nat v :+ Nat v
 | Nat v :* Nat v
instance Num (Nat v) where
 (+) = (:+)
 (*) = (:*)
 abs = id
 signum = error "signum Nat"
 fromInteger = error "fromInteger Nat"
 negate = error "negate Nat"
data Prop v
 = Ex (v -> Prop v)
 | Al (v -> Prop v)
 | Nat v := Nat v
 | Nat v :> Nat v
 | Nat v :< Nat v
 | Prop v :& Prop v
 | Prop v :| Prop v
 | Not (Prop v)
-- Display propositions in the given format.
allVars :: [String]
allVars = do
 s <- "" : allVars
 c <- ['a' .. 'z']
 pure (s ++ [c])
showNat :: Int -> Nat String -> ShowS
showNat _ (Var v) = showString v
showNat prec (a :+ b) =
 showParen (prec > 6) $ showNat 6 a . showString "+" . showNat 7 b
showNat prec (a :* b) =
 showParen (prec > 7) $ showNat 7 a . showString "*" . showNat 8 b
showProp :: Int -> Prop String -> [String] -> ShowS
showProp prec (Ex p) (v:free) =
 showParen (prec > 1) $ showString ("E " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (Al p) (v:free) =
 showParen (prec > 1) $ showString ("A " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (a := b) _ =
 showParen (prec > 4) $ showNat 5 a . showString "=" . showNat 5 b
showProp prec (a :> b) _ =
 showParen (prec > 4) $ showNat 5 a . showString ">" . showNat 5 b
showProp prec (a :< b) _ =
 showParen (prec > 4) $ showNat 5 a . showString "<" . showNat 5 b
showProp prec (p :& q) free =
 showParen (prec > 3) $
 showProp 4 p free . showString " & " . showProp 3 q free
showProp prec (p :| q) free =
 showParen (prec > 2) $
 showProp 3 p free . showString " | " . showProp 2 q free
showProp _ (Not p) free = showString "!" . showProp 9 p free
-- Compute the score.
scoreNat :: Nat v -> Int
scoreNat (Var _) = 1
scoreNat (a :+ b) = scoreNat a + 1 + scoreNat b
scoreNat (a :* b) = scoreNat a + 1 + scoreNat b
scoreProp :: Prop () -> Int
scoreProp (Ex p) = 2 + scoreProp (p ())
scoreProp (Al p) = 2 + scoreProp (p ())
scoreProp (p := q) = scoreNat p + 1 + scoreNat q
scoreProp (p :> q) = scoreNat p + 1 + scoreNat q
scoreProp (p :< q) = scoreNat p + 1 + scoreNat q
scoreProp (p :& q) = scoreProp p + 1 + scoreProp q
scoreProp (p :| q) = scoreProp p + 1 + scoreProp q
scoreProp (Not p) = 1 + scoreProp p
-- Convenience wrappers for n-ary exists and forall.
class OpenProp p where
 type OpenPropV p
 ex, al :: p -> Prop (OpenPropV p)
instance OpenProp (Prop v) where
 type OpenPropV (Prop v) = v
 ex = id
 al = id
instance (OpenProp p, a ~ Nat (OpenPropV p)) => OpenProp (a -> p) where
 type OpenPropV (a -> p) = OpenPropV p
 ex p = Ex (ex . p . Var)
 al p = Al (al . p . Var)
-- Utility for common subexpression elimination.
cse :: Int -> Nat v -> (Nat v -> Prop v) -> Prop v
cse uses x cont
 | (scoreNat x - 1) * (uses - 1) > 6 = ex (\x' -> x' := x :& cont x')
 | otherwise = cont x
-- p implies q.
infixl 1 ==>
p ==> q = Not p :| q
-- Define one as the unique n with n+n>n*n.
withOne ::
 ((?one :: Nat v) =>
 Prop v)
 -> Prop v
withOne p =
 ex
 (\one ->
 let ?one = one
 in one + one :> one * one :& p)
-- a is a multiple of d.
divides d a = ex (\b -> a := d * b)
-- a is a power of p (assuming p is prime).
powerOfPrime a p = al (\b -> b :> ?one :& divides b a ==> divides p b)
-- a is 0 or a digit of the base-p number s (assuming p is prime).
isDigit a s p =
 cse 2 a $ \a ->
 a :< p :&
 ex
 (\b -> powerOfPrime b p :& ex (\q r -> r :< b :& s := (p * q + a) * b + r))
-- An injection from N2 to N, for representing tuples.
pair a b = (a + b) ^ 2 + b
-- πn0/πd < π/4 < πn1/πd, with both fractions approaching π/4 as k
-- increases:
-- πn0 = 22·42·62⋯(2·k)2·k
-- πn1 = 22·42·62⋯(2·k)2·(k + 1)
-- πd = 12⋅32·52⋯(2·k + 1)2
πBound p k cont =
 ex
 (\s x πd ->
 al
 (\i ->
 (i := pair (k + k) x :| i := pair (k + k + ?one) πd ==>
 isDigit (i + ?one) s p) :&
 al
 (\a ->
 isDigit (pair i a + ?one) s p ==>
 ((i :< ?one + ?one :& a := ?one) :|
 ex
 (\i' a' ->
 isDigit (pair i' a' + ?one) s p :&
 i := i' + ?one + ?one :& a := i ^ 2 * a')))) :&
 let πn0 = x * k
 πn1 = πn0 + x
 in cont πn0 πn1 πd)
-- en0/ed < e < en1/ed, with both fractions approaching e as k
-- increases:
-- en0 = (k + 1)^k * k
-- en1 = (k + 1)^(k + 1)
-- ed = k^(k + 1)
eBound p k cont =
 ex
 (\s x ed ->
 cse 3 (pair x ed) (\y -> isDigit (pair k y + ?one) s p) :&
 al
 (\i a b ->
 cse 3 (pair a b) (\y -> isDigit (pair i y + ?one) s p) ==>
 (i :< ?one :& a := ?one :& b := k) :|
 ex
 (\i' a' b' ->
 cse 3 (pair a' b') (\y -> isDigit (pair i' y + ?one) s p) ==>
 i := i' + ?one :& a := (k + ?one) * a' :& b := k * b')) :&
 let en0 = x * k
 en1 = en0 + x
 in cont en0 en1 ed)
-- There exist a, b, c ∈ N (not all zero) with a·π/4 + b·e = c or
-- a·π/4 = b·e + c or b·e = a·π/4 + c.
prop :: Prop v
prop =
 withOne $
 ex
 (\a b c ->
 al
 (\p k ->
 k :< ?one :|
 (πBound p k $ \πn0 πn1 πd ->
 eBound p k $ \en0 en1 ed ->
 cse 3 (a * πn0 * ed) $ \x0 ->
 cse 3 (a * πn1 * ed) $ \x1 ->
 cse 3 (b * en0 * πd) $ \y0 ->
 cse 3 (b * en1 * πd) $ \y1 ->
 cse 6 (c * πd * ed) $ \z ->
 (x0 + y0 :< z :& x1 + y1 :> z) :|
 (x0 :< y1 + z :& x1 :> y0 + z) :|
 (y0 :< x1 + z :& y1 :> x0 + z))))
main :: IO ()
main = do
 print (scoreProp prop)
 putStrLn (showProp 0 prop allVars "")

Try it online!

• Ørjan Johansen: "which is satisfied iff a = 1, or p is prime and a is a power of it" - you can also have p = 1. Although p > 1 is implied by isDigit, the only place you use it.
• Anders Kaseorg: @ØrjanJohansen Thanks, I fixed that note. (It actually doesn’t matter which sets powerOfPrime and isDigit wind up representing in unexpected cases, as long as there’s some way to represent every finite set.)
• Ørjan Johansen: If a has score 7 or higher, I think, then it will be worth adding an ex (\a' -> a' := a :& ... ) wrapper to isDigit.
• Anders Kaseorg: @ØrjanJohansen Sure, that saves 68. Thanks!
• Ørjan Johansen: I believe you need to require k>0, as eBound gives a zero denominator (and one zero numerator) in the k==0 case, so all the alternatives fail.

Answer 2

270

E1 { Exist 1, defined when Any k introduced }
Ec1 Ec2 Ec3 Ec4 Ec5 Ak k*1=k & c3>1 & ( En0 An n<n0 | { for large enough n, |(c1-c4)e+c3(4-pi)/8+(c2-c5)|<1/k }
Ex Ep Ew Emult At (Eb ((b>1 & Eh b*h=t) &! Eh h*p=b)) | { x read in base-p, then each digit in base-w. t as a digit }
Ee1 Ee2 Ehigher Elower e2<p & lower<t & ((higher*p+e1)*p+e2)*t+lower=x & { last digit e1, this digit e2 }
 { Can infer that e2=w+1 | e1<=e2 & u1<=u2 & i1<=i2 & s1<=s2 & t1<=t2, so some conditions omitted }
Ei1 Es1 Et1 Eu1 (((u1*w)+i1)*w+t1)*w+s1=e1 & { (u,i,t,s) }
Ei2 Es2 Et2 Eu2 i2<w & s2<w & t2<w & (((u2*w)+i2)*w+t2)*w+s2=e2 & { e2=1+w is initial state u=i=0, s=t=1 }
(e2=w+1 | e1=e2 | i2=i1+1+1 & s2=s1*(n+1) & t2=t1*n & { i=2n, s=(n+1)^n, mult=t=n^n, s/mult=e }
Eg1 Eg2 g1+1=(i2+i2)*(i2+i2) & g1*u1+mult=g1*u2+g2 & g2<g1) & { u/mult=sum[j=4,8,...,4n]1/(j*j-1)=(4-pi)/8. mult=g1*(u2-u1)+g2 }
(t>1 | i2=n+n & t2=mult & Ediff Ediff2 { check at an end t=1 }
c1*s2+c2*mult+c3*u2+diff=c4*s2+c5*mult+diff2 & k*(diff+diff2)<mult)) { |diff-diff2|<=diff+diff2<mult/k, so ...<1/k }

a|b&c is a|(b&c) since I think removing these parentheses makes it look better, anyway they're free.

Used JavaScript "(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g) to count tokens.

• Anders Kaseorg: Why can you take mult = t? Also since x can only have finitely many digits, you’ll need to allow for e1 = e2 = 0 for sufficiently large t. Also you’ll need more parentheses or other disambiguation for ambiguous constructs like _ & _ | _.
• l4m2: @AndersKaseorg I multiply every item mult. Don't see any problem mult=t2 at the end. e1=e2=0 should be fixed but not that certain, so I currently don't change the acception.
• Anders Kaseorg: If a & b | c is (a & b) | c then your t*1=t is definitely in the wrong place. Also you haven't excluded the trivial solution c1 = c4 & c2 = c5 & c3 = 0 & diff = diff2.
• l4m2: @AndersKaseorg Do my reason why diff≠diff2 work?
• l4m2: Anyway I can use !(c2=c5) as we already know e is irrational, so even if this don't work score won't increase