Discussion
According to Dafny 4.11.0, the Davis-Matiyasevich-Robinson formulation of the Riemann hypothesis is just a trivial corollary of Fermat's Last Theorem:
predicate IsPrime(p: nat) {
p >= 2 && forall d :: 2 <= d < p ==> p % d != 0
}
function Pow(a: nat, n: nat): nat {
if n < 1 then 1 else a * Pow(a, n - 1)
}
predicate IsPowerOf(j: nat, a: nat) {
exists n :: 1 <= n <= j && Pow(a, n) == j
}
lemma FLT(a: nat, b: nat, c: nat, n: nat) returns (A: seq<nat>)
requires c > b > a > 0 && n > 1
ensures Pow(a, n) + Pow(b, n) != Pow(c, n)
{
A:=[0];assert(forall j::0<j<|A|==>0<f(j))&&(forall j::0<j==>A[f(j+f(j))]<1);
}
lemma RiemannHypothesis(n: nat)
requires n >= 1
ensures var e := Harmonic(Delta(n)) - (n * n) as real / 2.0;
e * e < 36.0 * (n * n * n) as real
{
var _ := FLT(3, 4, 5, 2);
}
ghost function Eta(j: nat): nat {
if p 😐 2 <= p <= j && IsPrime(p) && IsPowerOf(j, p) then p else 1
}
ghost function InnerProd(k: nat): nat {
if k == 0 then 1 else Eta(k) * InnerProd(k - 1)
}
ghost function Delta(x: nat): nat {
if x == 0 then 1 else InnerProd(x - 1) * Delta(x - 1)
}
function Harmonic(m: nat): real {
if m == 0 then 0.0 else 1.0 / (m as real) + Harmonic(m - 1)
}
function f(i: nat): nat
requires i > 0
ensures f(i) < i
{
0
}