diff --git a/Src/Problem40.lean b/Src/Problem40.lean index 7d60fdf..6d84c23 100644 --- a/Src/Problem40.lean +++ b/Src/Problem40.lean @@ -3,17 +3,24 @@ (Intermediate ๐ŸŒŸ๐ŸŒŸ) Goldbach's conjecture says that every positive even number greater than `2` is the sum of two prime numbers. Example: `28 = 5 + 23`. It is one of the most famous facts in number theory that has not been proved to be correct in the general case. It has been numerically confirmed up to very large numbers (much larger than we can go with our Prolog system). Write a predicate to find the two prime numbers that sum up to a given even integer. -/ -def Nat.isPrime (n : Nat) : Bool := - if n == 0 || n == 1 then - false - else - let properDivisors := List.range n - |>.drop 2 - |>.filter (n % ยท == 0) - properDivisors.length == 0 +def Nat.isPrime (n : Nat) : Bool := Id.run do + if n โ‰ค 2 then + return false + for d in [2:n] do + if n % d = 0 then + return false + if d ^ 2 > n then + break + return true + +-- You can use this! +#check Nat.isPrime def goldbach (n : Nat) : Nat ร— Nat := Id.run do -- sorry + if n % 2 โ‰  0 then + panic! "n must be an even number" + for cand in (List.range n) do if not cand.isPrime then continue @@ -41,3 +48,5 @@ def goldbachTest (n : Nat) : IO Unit := #eval goldbachTest 308 #eval goldbachTest 308000 + +#eval goldbachTest 19278020 diff --git a/Src/Problem41.lean b/Src/Problem41.lean new file mode 100644 index 0000000..06a13b4 --- /dev/null +++ b/Src/Problem41.lean @@ -0,0 +1,42 @@ +/- # Problem 40 + +(Intermediate ๐ŸŒŸ๐ŸŒŸ) A list of even numbers and their Goldbach compositions in a given range. +-/ + +def Nat.isPrime (n : Nat) : Bool := Id.run do + if n โ‰ค 2 then + return false + for d in [2:n] do + if n % d = 0 then + return false + if d ^ 2 > n then + break + return true + +def goldbach (n : Nat) : Nat ร— Nat := Id.run do + for cand in [2:n] do + if not cand.isPrime then + continue + let rest := n - cand + if not rest.isPrime then + continue + return (cand, rest) + + panic! "we've found a counter example of goldbach conjecture!! ๐ŸŽ‰" + +def goldbachList (lower upper : Nat) (primeLower : Nat := 2) : List (Nat ร— Nat) := + -- sorry + List.range (upper + 1) + |>.filter (ยท โ‰ฅ lower) + |>.filter (ยท % 2 == 0) + |>.map (fun n => (goldbach n)) + |>.filter (fun t => t.fst > primeLower) + -- sorry + +-- The following codes are for test and you should not edit these. + +#guard goldbachList 9 20 == [(3, 7), (5, 7), (3, 11), (3, 13), (5, 13), (3, 17)] + +#guard goldbachList 9 20 3 == [(5, 7), (5, 13)] + +#guard goldbachList 4 2000 50 == [(73,919),(61,1321),(67,1789),(61,1867)] diff --git a/Src/Problem46.lean b/Src/Problem46.lean new file mode 100644 index 0000000..0b99345 --- /dev/null +++ b/Src/Problem46.lean @@ -0,0 +1,24 @@ +/- # Problem 46 +(Intermediate ๐ŸŒŸ๐ŸŒŸ) Truth tables for logical expressions. +-/ + + +def table (p : Bool โ†’ Bool โ†’ Bool) : List (List Bool) := + -- sorry + [ + [true, true, p true true], + [true, false, p true false], + [false, true, p false true], + [false, false, p false false] + ] + -- sorry + +-- The following codes are for test and you should not edit these. + +#guard table (fun a b => And a (Or a b)) == + [ + [true, true, true], + [true, false, true], + [false, true, false], + [false, false, false] + ] diff --git a/md/SUMMARY.md b/md/SUMMARY.md index 1b0f7c4..708b87e 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -51,4 +51,9 @@ * [37: Euler's totient improved](./build/Problem37.md) * [38: Compare totient calculations]() * [39: Prime numbers in a range](./build/Problem39.md) -* [40: Goldbach's conjecture](./build/Problem40.md) \ No newline at end of file +* [40: Goldbach's conjecture](./build/Problem40.md) +* [41: Goldbach's list](./build/Problem41.md) + +# 46-50: Logic and codes + +* [46: Truth table](./build/Problem46.md) \ No newline at end of file