badge: proved

source:
import Mathlib
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :=
  (Nat.prime_two).irrational_sqrt

status: ok

tool: lean


badge: ran

output: True

tool: python


output: (True, 147573952589676412927)


source:
import Mathlib
theorem finite_division_ring_comm (D : Type*) [DivisionRing D] [Finite D] (a b : D) :
    a * b = b * a :=
  (littleWedderburn D).mul_comm a b


badge: refuted

output:
/work/Submission.lean:2:59: error: unsolved goals
⊢ False

source:
import Mathlib
theorem sqrt_four_irrational : Irrational (Real.sqrt 4) := by
  norm_num

status: failed


output:
INFINITY
True

source:
def colname(x):
    if x == 0:
        return ''
    else:
        (q, rm1) = divmod(x - 1, 26)
        return colname(q) + chr (ord ('A') + rm1)

a = 76686766181
print (colname (a))
print (colname (a) == 'INFINITY')


source:
import Mathlib

theorem testing : ∀ a b c d e : Nat, a + b + c + d + e = (c + (e + d)) + (b + a) := by
  intros
  abel


source:
import Mathlib

example : 1 + 1 = 2 := by
  norm_num


output:
/work/Submission.lean:3:23: error: unsolved goals
⊢ False

source:
import Mathlib

example : 1 + 1 = 3 := by
  norm_num


output:
I              = 15.83687034789483360405179196564431
(5/(2*sqrt3))*J = 15.83687034789483360405179196564431
closed form    = 15.83687034789483360405179196564431
max abs error  = 9.404 e-38

(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=1.00  rel 9.08 e-39
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=1.50  rel 3.29 e-38
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=2.50  rel 1.51 e-38
(5)  eta^4*th3^4 = 16*eta(2t)^8+eta(t/2)^8 at t=4.00  rel 1.21 e-38
(3)  I - 2^(4/3)*Pi*int g         9.32 e-27
(4)  J - 2^(4/3)*Pi*int t*g       2.72 e-28
(6)  int g - 10*A0                1.18 e-27
(7)  int t*g - 8*A1               3.44 e-29
(8)  A0 - 3/(2*Pi)*L(h,1)         7.35 e-40
(9)  A1 - 9/(4*Pi^2)*L(h,2)       0.e-39
(10) I - 15*2^(4/3)*L(h,1)        0.e-37
(11) J - 18*2^(4/3)/Pi*L(h,2)     4.70 e-38
     Lambda(s)-Lambda(4-s), s=1.3 1.47 e-39
(12) L(h,1) - 9/(2*Pi^2)*L(h,3)   0.e-38

(13) L(h,2): Mellin 0.759965749993307635913622747426
     mf pkg 0.759965749993307635913622747426
     Gamma(1/3)^9/(96*Pi^4)          0.759965749993307635913622747426
(14) L(h,3): Mellin 0.918950262785094625843347770476
     mf pkg 0.918950262785094625843347770476
     Gamma(1/3)^9/(144*sqrt(3)*Pi^3) 0.918950262785094625843347770476

tool: pari


output: (1.6449290668607264, 1.6449340668482264)


source:
import Mathlib

/-! The gravitoelectromagnetic constants carry the sign of G.

    εg = 1/(4πG) and μg = 4πG/c².  For any c ≠ 0 each is positive exactly when
    G is.  Nothing about the sources appears in either statement, so no choice
    of source term can move them. -/

theorem eps_g_sign (G : ℝ) : 0 < 1 / (4 * Real.pi * G) ↔ 0 < G := by
  have hpi : (0:ℝ) < 4 * Real.pi := by positivity
  rw [one_div_pos]
  constructor
  · intro h; nlinarith
  · intro h; nlinarith

theorem mu_g_sign (G c : ℝ) (hc : c ≠ 0) :
    0 < 4 * Real.pi * G / c ^ 2 ↔ 0 < G := by
  have hpi : (0:ℝ) < 4 * Real.pi := by positivity
  have hc2 : (0:ℝ) < c ^ 2 := by positivity
  rw [div_pos_iff]
  constructor
  · rintro (⟨h, _⟩ | ⟨_, h⟩)
    · nlinarith
    · nlinarith
  · intro h; exact Or.inl ⟨by nlinarith, hc2⟩


output:
[G]     = m^3 / (kg s^2)
[eps_g] = kg s^2 / m^3
[mu_g]  = m / kg

r_i / m_i                              = m / kg             != [G]
[phidot_g mu_g], as stated             = m^3 / (kg s)       != [G]
[phidot_g mu_g], from phi_g=m^2/s^2    = m^3 / (kg s^3)     != [G]

[mu_g] == [r_i/m_i]: True
any candidate has the dimensions of G: False

source:
# Dimensions as exponent vectors over (m, kg, s). No physics in here: this
# checks only that the stated dimensions are not the dimensions of G.
def mul(a, b): return tuple(x + y for x, y in zip(a, b))
def div(a, b): return tuple(x - y for x, y in zip(a, b))

def show(v):
    names = ('m', 'kg', 's')
    num = ' '.join(n if e == 1 else f'{n}^{e}' for n, e in zip(names, v) if e > 0)
    den = ' '.join(n if e == -1 else f'{n}^{-e}' for n, e in zip(names, v) if e < 0)
    if not den:
        return num or '1'
    return f'{num or 1} / ' + (f'({den})' if ' ' in den else den)

ONE = (0, 0, 0)
G   = (3, -1, -2)                   # m^3 / (kg s^2), by definition of G
c   = (1,  0, -1)
eps = div(ONE, G)                   # eps_g = 1/(4 pi G);   4 pi is dimensionless
mu  = div(G, mul(c, c))             # mu_g  = 4 pi G / c^2

phi = (2, 0, -2)                    # GEM scalar potential, m^2/s^2
phidot = div(phi, (0, 0, 1))
candidates = [
    ('r_i / m_i',                        (1, -1, 0)),
    ('[phidot_g mu_g], as stated',       (3, -1, -1)),
    ('[phidot_g mu_g], from phi_g=m^2/s^2', mul(phidot, mu)),
]

print(f'[G]     = {show(G)}')
print(f'[eps_g] = {show(eps)}')
print(f'[mu_g]  = {show(mu)}')
print()
for name, v in candidates:
    print(f'{name:38s} = {show(v):18s} {"== [G]" if v == G else "!= [G]"}')
print()
print('[mu_g] == [r_i/m_i]:', mu == (1, -1, 0))
print('any candidate has the dimensions of G:', any(v == G for _, v in candidates))


source:
import Mathlib

/-! The arithmetic of the fork — the part a kernel can see.

    The ΔL = 2 bilinears carry X-charge −6, and a `Z_N` remnant shifts a charge
    only by multiples of N.  So a Majorana operator survives exactly when
    `N ∣ 6`: `N = 6` allows it, `N = 12` forbids it to all orders, and the
    holonomy test that would certify Dirac is exactly `2q ≠ 0`. -/

/-- Dressing a −6 bilinear with powers of `Φ_N` can reach charge zero iff N ∣ 6. -/
theorem majorana_survives_iff (N : ℤ) : (∃ k : ℤ, -6 + N * k = 0) ↔ N ∣ 6 := by
  constructor
  · rintro ⟨k, hk⟩
    exact ⟨k, by linarith⟩
  · rintro ⟨k, hk⟩
    exact ⟨k, by linarith⟩

theorem allowed_at_six : ∃ k : ℤ, -6 + 6 * k = 0 := ⟨1, by norm_num⟩

/-- Not "not yet seen": no integer k works, so the operator is absent to all orders. -/
theorem forbidden_at_twelve : ¬ ∃ k : ℤ, -6 + 12 * k = 0 := by
  rintro ⟨k, hk⟩
  omega

/-- In the `Z_N` remnant a charge is its own conjugate exactly when `2q = 0`. -/
theorem self_conjugate_iff (N : ℕ) (q : ZMod N) : q = -q ↔ 2 * q = 0 := by
  rw [two_mul, eq_neg_iff_add_eq_zero]

/-- At q = −3 in `Z_12` it is not, which is what a Dirac certificate would measure. -/
theorem neutrino_is_not_self_conjugate : (-3 : ZMod 12) ≠ -(-3 : ZMod 12) := by
  decide