ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Computing $(1111 / 8093)$ by the Euclidean Jacobi algorithm

Example

The Euclidean Jacobi algorithm (The Euclidean algorithm computes the Jacobi symbol without factoring the denominator) evaluates

$(\frac{1111}{8093}) = - 1$

without factoring $8093$ . Its states $(ε, A, N)$ are

$(1, 1111, 8093), (1, 8093, 1111), (- 1, 1111, 79), (- 1, 79, 5), (- 1, 5, 1) .$

Facts & Assumptions

Given: The initial pair $(1111, 8093)$ with odd positive denominator.

[L1]

The Euclidean Jacobi algorithm terminates and returns $(\frac{a}{n})$ without factoring the odd denominator $n$ (The Euclidean algorithm computes the Jacobi symbol without factoring the denominator).

Verification

technique · direct

1.1L1givenalgebra

The divisions and sign updates are $8093 = 7 \cdot 1111 + 316$ , $316 = 2^{2} \cdot 79$ , $1111 = 14 \cdot 79 + 5$ , $79 = 15 \cdot 5 + 4$ , and $4 = 2^{2}$ . The first swap has no sign change, removing either square power of $2$ has no sign change, and the swap of $79$ and $1111$ changes the sign because both are $3$ modulo $4$ ; the next denominator is $1$ . After each complete update, these calculations give exactly the displayed state sequence.

2.1step 1.1L1∎

The terminal sign is $- 1$ , and [L1] identifies it with $(\frac{1111}{8093})$ . No factorisation of $8093$ occurs in step 1.1.

Depends on

The Euclidean algorithm computes the Jacobi symbol without factoring the denominator

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. Gorodnik, Number Theory, Lecture 10, Example 1.6 (standard reference, not scraped)
V. Shoup, A Computational Introduction to Number Theory and Algebra, 2nd ed., §12.3 (standard reference, not scraped)

Computing (1111/8093)(1111/8093) by the Euclidean Jacobi algorithm