Root triple brute-forcy script Slower than PyPy though ugh

Changes

2 changed files (+29/-0)

• RootTriple.lean (new)
  • @@ -0,0 +1,25 @@
    + def check n (A : Vector (Vector Bool n) n) := Id.run do + for ha : a in [:n] do + for hb : b in [a+1:n] do + for hc : c in [b+1:n] do + if (A[a][b] && A[b][c] && !A[a][c]) || (!A[a][b] && !A[b][c] && A[a][c]) || (A[a][b] && A[b][c] && A[a][c]) then + -- if (A[a][b] && A[b][c] && !A[a][c]) || (A[a][b] && !A[b][c] && !A[a][c]) || (!A[a][b] && A[b][c] && !A[a][c]) then + -- if (A[a][b] && A[b][c] && !A[a][c]) || (A[a][b] && !A[b][c] && !A[a][c]) || (!A[a][b] && A[b][c] && !A[a][c]) || (A[a][b] && A[b][c] && A[a][c]) then + return false + return true + + def f n := Id.run do + let mut ans := 0 + for i in [:2^(n*(n-1)/2)] do + let mut A := Vector.replicate n (Vector.replicate n true) + let mut cnt := 0 + for ha : a in [:n] do + for hb : b in [a+1:n] do + A := A.set a <| A[a].set b <| i >>> cnt &&& 1 == 1 + cnt := cnt + 1 + ans := ans + (check n A).toNat + return ans + + def main := do + for i in [1:8] do + IO.println <| f i
• lakefile.toml
  • @@ -22,6 +22,10 @@ root = "Gcd"
    name = "commitgraph" root = "CommitGraph" + [[lean_exe]] + name = "roottriple" + root = "RootTriple" + [[require]] name = "mathlib" scope = "leanprover-community"