19
\$\begingroup\$

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 challenge. Answers are not required to contain code.
  • This is similar to, but not, a 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
\$\endgroup\$
  • 5
    \$\begingroup\$ 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. \$\endgroup\$ – xnor Jan 4 '18 at 5:30
  • 1
    \$\begingroup\$ 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)? \$\endgroup\$ – Luis Mendo Jan 4 '18 at 13:23
  • 1
    \$\begingroup\$ 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 \$\endgroup\$ – l4m2 Jan 4 '18 at 13:38
  • 1
    \$\begingroup\$ 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). \$\endgroup\$ – Lynn Jan 6 '18 at 13:55
  • \$\begingroup\$ 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 \$\endgroup\$ – l4m2 Mar 8 '18 at 17:25
27
\$\begingroup\$

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 ∈ ℕ (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 π₀ < π < π₁ and e₀ < e < e₁, we have a·π₀ + b·e₀ < c < a·π₁ + b·e₁ or a·π₀ − b·e₁ < c < a·π₁ + b·e₀ or −a·π₁ + b·e₀ < c < −a·π₀ + b·e₁. (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 ℕ² to ℕ, for representing tuples.
pair a b = (a + b) ^ 2 + b

-- πn₀/πd < π/4 < πn₁/πd, with both fractions approaching π/4 as k
-- increases:
-- πn₀ = 2²·4²·6²⋯(2·k)²·k
-- πn₁ = 2²·4²·6²⋯(2·k)²·(k + 1)
-- πd = 1²⋅3²·5²⋯(2·k + 1)²
π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 πn₀ = x * k
           πn₁ = πn₀ + x
       in cont πn₀ πn₁ πd)

-- en₀/ed < e < en₁/ed, with both fractions approaching e as k
-- increases:
-- en₀ = (k + 1)^k * k
-- en₁ = (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 en₀ = x * k
           en₁ = en₀ + x
       in cont en₀ en₁ ed)

-- There exist a, b, c ∈ ℕ (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 $ \πn₀ πn₁ πd ->
               eBound p k $ \en₀ en₁ ed ->
                 cse 3 (a * πn₀ * ed) $ \x₀ ->
                   cse 3 (a * πn₁ * ed) $ \x₁ ->
                     cse 3 (b * en₀ * πd) $ \y₀ ->
                       cse 3 (b * en₁ * πd) $ \y₁ ->
                         cse 6 (c * πd * ed) $ \z ->
                           (x₀ + y₀ :< z :& x₁ + y₁ :> z) :|
                           (x₀ :< y₁ + z :& x₁ :> y₀ + z) :|
                           (y₀ :< x₁ + z :& y₁ :> x₀ + z))))

main :: IO ()
main = do
  print (scoreProp prop)
  putStrLn (showProp 0 prop allVars "")

Try it online!

\$\endgroup\$
  • \$\begingroup\$ "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. \$\endgroup\$ – Ørjan Johansen Jan 7 '18 at 1:11
  • \$\begingroup\$ @Ø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.) \$\endgroup\$ – Anders Kaseorg Jan 7 '18 at 2:06
  • 2
    \$\begingroup\$ If a has score 7 or higher, I think, then it will be worth adding an ex (\a' -> a' := a :& ... ) wrapper to isDigit. \$\endgroup\$ – Ørjan Johansen Jan 7 '18 at 2:06
  • \$\begingroup\$ @ØrjanJohansen Sure, that saves 68. Thanks! \$\endgroup\$ – Anders Kaseorg Jan 7 '18 at 2:21
  • \$\begingroup\$ 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. \$\endgroup\$ – Ørjan Johansen Jan 7 '18 at 3:04
3
\$\begingroup\$

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.

\$\endgroup\$
  • \$\begingroup\$ 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 _ & _ | _. \$\endgroup\$ – Anders Kaseorg Oct 25 at 11:07
  • \$\begingroup\$ @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. \$\endgroup\$ – l4m2 Oct 25 at 16:19
  • \$\begingroup\$ 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. \$\endgroup\$ – Anders Kaseorg Oct 25 at 19:32
  • \$\begingroup\$ @AndersKaseorg Do my reason why diff≠diff2 work? \$\endgroup\$ – l4m2 Oct 26 at 9:55
  • \$\begingroup\$ Anyway I can use !(c2=c5) as we already know e is irrational, so even if this don't work score won't increase \$\endgroup\$ – l4m2 Oct 26 at 11:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.