Write it into number theory style
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!
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.