Write it into number theory style
671

E a (a+a&gt;a*a &amp; (E b (E c (E d (A e (A f (f&lt;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&lt;e &amp; (E k ((A l (!(l&gt;a &amp; (E m k=l*m)) | (E m l=e*m))) &amp; (E l (E m (m&lt;k &amp; g=(e*l+(j+a))*k+m)))))) &amp; (A k (!(E l (l=(j+k)*(j+k)+k+a &amp; l&lt;e &amp; (E m ((A n (!(n&gt;a &amp; (E o m=n*o)) | (E o n=e*o))) &amp; (E n (E o (o&lt;m &amp; g=(e*n+l)*m+o))))))) | j&lt;a+a &amp; k=a | (E l (E m ((E n (n=(l+m)*(l+m)+m+a &amp; n&lt;e &amp; (E o ((A p (!(p&gt;a &amp; (E q o=p*q)) | (E q p=e*q))) &amp; (E p (E q (q&lt;o &amp; g=(e*p+n)*o+q))))))) &amp; j=l+a+a &amp; k=j*j*m))))))) &amp; (E j (E k (E l ((E m (m=(k+l)*(k+l)+l &amp; (E n (n=(f+m)*(f+m)+m+a &amp; n&lt;e &amp; (E o ((A p (!(p&gt;a &amp; (E q o=p*q)) | (E q p=e*q))) &amp; (E p (E q (q&lt;o &amp; j=(e*p+n)*o+q))))))))) &amp; (A m (A n (A o (!(E p (p=(n+o)*(n+o)+o &amp; (E q (q=(m+p)*(m+p)+p+a &amp; q&lt;e &amp; (E r ((A s (!(s&gt;a &amp; (E t r=s*t)) | (E t s=e*t))) &amp; (E s (E t (t&lt;r &amp; j=(e*s+q)*r+t))))))))) | m&lt;a &amp; n=a &amp; o=f | (E p (E q (E r (!(E s (s=(q+r)*(q+r)+r &amp; (E t (t=(p+s)*(p+s)+s+a &amp; t&lt;e &amp; (E u ((A v (!(v&gt;a &amp; (E w u=v*w)) | (E w v=e*w))) &amp; (E v (E w (w&lt;u &amp; j=(e*v+t)*u+w))))))))) | m=p+a &amp; n=(f+a)*q &amp; o=f*r)))))))) &amp; (E m (m=b*(h*f)*l &amp; (E n (n=b*(h*f+h)*l &amp; (E o (o=c*(k*f)*i &amp; (E p (p=c*(k*f+k)*i &amp; (E q (q=d*i*l &amp; (m+o&lt;q &amp; n+p&gt;q | m&lt;p+q &amp; n&gt;o+q | o&lt;n+q &amp; p&gt;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 π₀ &lt; π &lt; π₁ and e₀ &lt; e &lt; e₁, we have a·π₀ + b·e₀ &lt; c &lt; a·π₁ + b·e₁ or a·π₀ − b·e₁ &lt; c &lt; a·π₁ + b·e₀ or −a·π₁ + b·e₀ &lt; c &lt; −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) &lt; π/2 &lt; 2/1 · 2/3 · 4/3 · 4/5 ⋯ (2·k)/(2·k + 1) · (2·k + 2)/(2·k + 1),

((k + 1)/k)k &lt; e &lt; ((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 &lt; p and ∃b, (powerOfPrime(b, p) and ∃q r, (r &lt; 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 :&amp;

infix 4 :=

infix 4 :&gt;

infix 4 :&lt;

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 -&gt; Prop v)
  | Al (v -&gt; Prop v)
  | Nat v := Nat v
  | Nat v :&gt; Nat v
  | Nat v :&lt; Nat v
  | Prop v :&amp; Prop v
  | Prop v :| Prop v
  | Not (Prop v)

-- Display propositions in the given format.
allVars :: [String]
allVars = do
  s &lt;- "" : allVars
  c &lt;- ['a' .. 'z']
  pure (s ++ [c])

showNat :: Int -&gt; Nat String -&gt; ShowS
showNat _ (Var v) = showString v
showNat prec (a :+ b) =
  showParen (prec &gt; 6) $ showNat 6 a . showString "+" . showNat 7 b
showNat prec (a :* b) =
  showParen (prec &gt; 7) $ showNat 7 a . showString "*" . showNat 8 b

showProp :: Int -&gt; Prop String -&gt; [String] -&gt; ShowS
showProp prec (Ex p) (v:free) =
  showParen (prec &gt; 1) $ showString ("E " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (Al p) (v:free) =
  showParen (prec &gt; 1) $ showString ("A " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (a := b) _ =
  showParen (prec &gt; 4) $ showNat 5 a . showString "=" . showNat 5 b
showProp prec (a :&gt; b) _ =
  showParen (prec &gt; 4) $ showNat 5 a . showString "&gt;" . showNat 5 b
showProp prec (a :&lt; b) _ =
  showParen (prec &gt; 4) $ showNat 5 a . showString "&lt;" . showNat 5 b
showProp prec (p :&amp; q) free =
  showParen (prec &gt; 3) $
  showProp 4 p free . showString " &amp; " . showProp 3 q free
showProp prec (p :| q) free =
  showParen (prec &gt; 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 -&gt; Int
scoreNat (Var _) = 1
scoreNat (a :+ b) = scoreNat a + 1 + scoreNat b
scoreNat (a :* b) = scoreNat a + 1 + scoreNat b

scoreProp :: Prop () -&gt; Int
scoreProp (Ex p) = 2 + scoreProp (p ())
scoreProp (Al p) = 2 + scoreProp (p ())
scoreProp (p := q) = scoreNat p + 1 + scoreNat q
scoreProp (p :&gt; q) = scoreNat p + 1 + scoreNat q
scoreProp (p :&lt; q) = scoreNat p + 1 + scoreNat q
scoreProp (p :&amp; 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 -&gt; Prop (OpenPropV p)

instance OpenProp (Prop v) where
  type OpenPropV (Prop v) = v
  ex = id
  al = id

instance (OpenProp p, a ~ Nat (OpenPropV p)) =&gt; OpenProp (a -&gt; p) where
  type OpenPropV (a -&gt; p) = OpenPropV p
  ex p = Ex (ex . p . Var)
  al p = Al (al . p . Var)

-- Utility for common subexpression elimination.
cse :: Int -&gt; Nat v -&gt; (Nat v -&gt; Prop v) -&gt; Prop v
cse uses x cont
  | (scoreNat x - 1) * (uses - 1) &gt; 6 = ex (\x' -&gt; x' := x :&amp; cont x')
  | otherwise = cont x

-- p implies q.
infixl 1 ==&gt;

p ==&gt; q = Not p :| q

-- Define one as the unique n with n+n&gt;n*n.
withOne ::
     ((?one :: Nat v) =&gt;
        Prop v)
  -&gt; Prop v
withOne p =
  ex
    (\one -&gt;
       let ?one = one
       in one + one :&gt; one * one :&amp; p)

-- a is a multiple of d.
divides d a = ex (\b -&gt; a := d * b)

-- a is a power of p (assuming p is prime).
powerOfPrime a p = al (\b -&gt; b :&gt; ?one :&amp; divides b a ==&gt; 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 -&gt;
    a :&lt; p :&amp;
    ex
      (\b -&gt; powerOfPrime b p :&amp; ex (\q r -&gt; r :&lt; b :&amp; s := (p * q + a) * b + r))

-- An injection from ℕ² to ℕ, for representing tuples.
pair a b = (a + b) ^ 2 + b

-- πn₀/πd &lt; π/4 &lt; π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 -&gt;
       al
         (\i -&gt;
            (i := pair (k + k) x :| i := pair (k + k + ?one) πd ==&gt;
             isDigit (i + ?one) s p) :&amp;
            al
              (\a -&gt;
                 isDigit (pair i a + ?one) s p ==&gt;
                 ((i :&lt; ?one + ?one :&amp; a := ?one) :|
                  ex
                    (\i' a' -&gt;
                       isDigit (pair i' a' + ?one) s p :&amp;
                       i := i' + ?one + ?one :&amp; a := i ^ 2 * a')))) :&amp;
       let πn₀ = x * k
           πn₁ = πn₀ + x
       in cont πn₀ πn₁ πd)

-- en₀/ed &lt; e &lt; 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 -&gt;
       cse 3 (pair x ed) (\y -&gt; isDigit (pair k y + ?one) s p) :&amp;
       al
         (\i a b -&gt;
            cse 3 (pair a b) (\y -&gt; isDigit (pair i y + ?one) s p) ==&gt;
            (i :&lt; ?one :&amp; a := ?one :&amp; b := k) :|
            ex
              (\i' a' b' -&gt;
                 cse 3 (pair a' b') (\y -&gt; isDigit (pair i' y + ?one) s p) ==&gt;
                 i := i' + ?one :&amp; a := (k + ?one) * a' :&amp; b := k * b')) :&amp;
       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 -&gt;
       al
         (\p k -&gt;
            k :&lt; ?one :|
            (πBound p k $ \πn₀ πn₁ πd -&gt;
               eBound p k $ \en₀ en₁ ed -&gt;
                 cse 3 (a * πn₀ * ed) $ \x₀ -&gt;
                   cse 3 (a * πn₁ * ed) $ \x₁ -&gt;
                     cse 3 (b * en₀ * πd) $ \y₀ -&gt;
                       cse 3 (b * en₁ * πd) $ \y₁ -&gt;
                         cse 6 (c * πd * ed) $ \z -&gt;
                           (x₀ + y₀ :&lt; z :&amp; x₁ + y₁ :&gt; z) :|
                           (x₀ :&lt; y₁ + z :&amp; x₁ :&gt; y₀ + z) :|
                           (y₀ :&lt; x₁ + z :&amp; y₁ :&gt; x₀ + z))))

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


Try it online!