The corpus, up close.

Real pairs, shown the way reviewers see them. Filter by verdict to read the human rationale behind each call.

• faithful

  source · LaTeX

  Let \(a, b \in \mathbb{R}_{\ge 0}\). Then \(\sqrt{ab} \le \tfrac{a+b}{2}\).

  formalization · Lean 4

  theorem sqrt_mul_le_half_add (a b : ℝ)
      (ha : 0 ≤ a) (hb : 0 ≤ b) :
      Real.sqrt (a * b) ≤ (a + b) / 2 := by
    nlinarith [Real.sq_sqrt (mul_nonneg ha hb),
      Real.sqrt_nonneg (a * b), sq_nonneg (a - b)]

  verdict rationale · human review

  Everything the informal statement asserts survives translation. Both variables range over nonnegative reals, matching the hypothesis; the geometric and arithmetic means appear on the correct sides; no hypothesis is added or dropped. The proof closes without sorry. Certified faithful.

• unfaithful

  source · LaTeX

  There are infinitely many primes \(p\) with \(p \equiv 3 \pmod{4}\).

  formalization · Lean 4

  -- statement drift: congruence condition dropped
  theorem primes_three_mod_four :
      ∀ n : ℕ, ∃ p, n < p ∧ Nat.Prime p := by
    intro n
    obtain ⟨p, hle, hp⟩ :=
      Nat.exists_infinite_primes (n + 1)
    exact ⟨p, hle, hp⟩

  verdict rationale · human review

  The informal claim is about primes congruent to 3 mod 4. The Lean statement proves that primes are infinite with the congruence condition dropped entirely. That is a true theorem, and the compiler accepts it, but it is a strictly weaker one: the congruence class is the whole content of the claim. Rejected as unfaithful.