What was already known
Faith, Cozzens and Faith, and Damiano had left open whether every right PCI ring is left PCI. Cozzens and Faith also asked whether a left V-domain must be right V; earlier symmetry implications required extra Ore or Noetherian hypotheses.
AI involvement
The author says Claude models produced the mathematical construction, manuscript, Lean code and metadata at his direction. His role in directing and submitting is acknowledged; the source does not document task-only autonomy.
Vlad Tsyrklevich states that Claude models produced the mathematics, manuscript and Lean code at his direction; the human reviewed the Challenge statement and submitted the project, but no human expert has checked the mathematics.
Importance
Provides counterexamples to two longstanding left-right symmetry questions in noncommutative ring theory.
Limitations
The entire paper and Lean proof library were machine-written by Claude under Vlad Tsyrklevich’s direction. The project says no human expert has checked the mathematics; a human reviewed only the Challenge statement. The compared Lean theorem covers the countable-domain, PCI, V-ring and non-right-Ore properties, but does not encode the paper’s additional claims that the ring is simple, principal on the left, left Noetherian, left hereditary or specifically an Ore extension.
Technical verification
The source reports a Lean proof library, completed Solution module, and Comparator checks matching the three main existence and asymmetry statements to Challenge. The assessed claim is the compared core theorem. Additional paper properties—simple, principal left ideal, left Noetherian, left hereditary, and explicit Ore-extension form—are outside the compared statement.
Formal checking
Palomar-registered source reports Lean comparator statement/axiom checks for the three exact existence and corollary theorems; the compared scope excludes extra structural properties.
- Checker
- Lean 4 kernel and Comparator as reported by the source repository and Palomar registry
- Scope
- Existence of a countable left PCI, left V domain that is not right Ore, PCI or V, plus asymmetry corollaries
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The maintainer positively states no human has checked the mathematics; only the Challenge statement was human-reviewed. No human explanation of the construction’s free-field and pseudo-linear-equation mechanism is documented.
Correction and publication history
Original construction, prior open questions, AI authorship and exact compared Lean statements reviewed; non-notifying local inclusion.
Read this published revision