Tulis pernyataan matematika, menggunakan simbol:

• There exists at least one non-negative integer(ditulis sebagai E, penjumlahan eksistensial)
• All non-negative integers(ditulis sebagai A, quantifier universal)
• + (tambahan)
• * (perkalian)
• = (persamaan)
• >, <(operator pembanding)
• &(dan), |(atau), !(tidak)
• (, )(untuk pengelompokan)
• nama variabel

yang setara dengan pernyataan itu

Ada bilangan rasional a, sehingga π + e * a adalah rasional.

(tentu saja, $\pi =3.1415...$ adalah konstanta matematika yang sama dengan keliling dibagi dengan diameter lingkaran, dan adalah angka Euler )$e=2.7182...$

Anda harus membuktikan bahwa pernyataan Anda memang setara dengan pernyataan di atas.

Jelas, cara "terpendek" untuk menyelesaikan ini adalah dengan membuktikan pernyataan itu benar atau salah, dan kemudian menjawab dengan pernyataan yang benar atau salah, karena semua pernyataan benar setara satu sama lain, seperti semua pernyataan salah.

Namun, nilai kebenaran pernyataan yang diberikan adalah masalah yang belum terpecahkan dalam matematika : kita bahkan tidak tahu apakah tidak rasional! Oleh karena itu, kecuali penelitian matematika terobosan, tantangannya adalah untuk menemukan pernyataan setara "sederhana", membuktikan kesetaraannya, dan menggambarkannya sesingkat mungkin.$\pi+e$

Mencetak gol

E A + * = > < & |dan !masing - masing menambahkan 1 pada skor. (dan )jangan menambahkan apa pun pada skor. Setiap nama variabel menambahkan 1 pada skor.

Misalnya, E x (A ba x+ba>x*(x+ba))skor 13 ( E x A ba x + ba > x * x + ba)

Skor terendah menang.

catatan:

_{Penafian: Catatan ini tidak ditulis oleh OP.}

• Ini bukan sebuah kode-golf tantangan. Jawaban tidak wajib mengandung kode.
• Ini mirip dengan, tetapi tidak, tantangan golf bukti , karena Anda perlu menulis pernyataan dan membuktikannya setara dengan pernyataan lain.
• Anda diperbolehkan mengirimkan pernyataan trivially-true (mis. Untuk semua x, x = x Ax x=x) atau pernyataan trivially-false (mis., Untuk semua x, x> x Ax x>x) jika Anda dapat membuktikan pernyataan di atas benar / salah.
• Anda diizinkan untuk menggunakan simbol tambahan (mirip dengan lemma dalam golf bukti), tetapi skornya akan dihitung sama dengan Anda tidak menggunakannya.
  Misalnya, jika Anda mendefinisikan a => bmean (!a) | b, setiap kali Anda menggunakan =>bukti Anda, skor Anda meningkat 2.

• Karena konstanta tidak terdaftar dalam simbol yang diizinkan, Anda tidak boleh menggunakannya.
  Sebagai contoh: Pernyataan 1 > 0dapat ditulis sebagai

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

  pada skor 23. (ingat bahwa =>biaya 2 per penggunaan).

Petunjuk

• Untuk menggunakan konstanta alami, Anda dapat melakukannya E0, 0+0=0 & E1, At 1*t=t &(jadi Anda tidak perlu =>yang lebih ekspansif); untuk angka yang lebih besar dari 1, tambahkan saja 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))))))))))))))))))))))))))

Bagaimana itu bekerja

Pertama, gandakan melalui penyebut yang konon berasal dari a dan (π + e · a) untuk menulis ulang kondisi sebagai: ada a, b, c ∈ ℕ (tidak semuanya nol) dengan a · π + b · e = c atau a · π - b · e = c atau −a · π + b · e = c. Tiga kasus diperlukan untuk menangani masalah tanda.

Maka kita perlu menulis ulang ini untuk berbicara tentang π dan e melalui perkiraan rasional: untuk semua perkiraan rasional π₀ <π <π₁ dan e₀ <e <e₁, kita memiliki · π₀ + b · e · <c <a · π₁ + b · e₁ atau a · π₀ - b · e₁ <c <a · π₁ + b · e₀ atau −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Perhatikan bahwa kami sekarang mendapatkan kondisi "tidak semuanya nol" gratis.)

Sekarang untuk bagian yang sulit. Bagaimana kita mendapatkan perkiraan rasional ini? Kami ingin menggunakan formula seperti

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} ,

tetapi tidak ada cara yang jelas untuk menulis definisi berulang dari produk-produk ini. Jadi kami membangun sedikit mesin yang pertama kali saya jelaskan di pos Quora ini . Menetapkan:

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

powerOfPrime (a, p): = ∀b, ((b> 1 dan membagi (b, a)) ⇒ membagi (p, b)),

yang terpenuhi iff a = 1, atau p = 1, atau p adalah prima dan a adalah kekuatannya. Kemudian

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

puas jika a = 0, atau a adalah angka dari basa-p s. Ini memungkinkan kami merepresentasikan set terbatas apa pun menggunakan digit beberapa nomor base-p. Sekarang kita dapat menerjemahkan perhitungan iteratif dengan menulis, secara kasar, ada sekumpulan keadaan peralihan sedemikian sehingga keadaan akhir ada di dalam himpunan, dan setiap keadaan dalam himpunan adalah keadaan awal atau mengikuti dalam satu langkah dari beberapa keadaan lain di dalam set.

Detail ada dalam kode di bawah ini.

Menghasilkan kode di 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 "")

Cobalah 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&cadalah a|(b&c)karena saya pikir menghapus tanda kurung ini membuatnya terlihat lebih baik, toh itu gratis.

JavaScript yang digunakan "(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)untuk menghitung token.