What was already known
Yoshinaga’s criterion was known. The human authors independently supplied the main-text Zariski-section proof of the same local obstructions and the global transfer argument.
AI involvement
The authors say the Yoshinaga-based appendix proof first arose in a guided ChatGPT 5.5 Plus conversation. They do not identify which individual sign vectors or lemmas were model-origin and which were added during correction.
The retained alternative proof arose from the guided model dialogue, while substantial human correction and the independent main proof prevent attributing the global theorem to AI.
Importance
Provides a complementary proof of the local ingredient.
Limitations
The authors verified and corrected the guided model proof; the model’s exact surviving steps are not itemized. The global non-asphericity theorem is the authors’ separate work.
Technical verification
The four authors expressly report verifying and correcting the appendix argument, including its two local obstructions. This is a source-reported human check of that final alternative proof, not a machine check or a check of all broader consequences by AIProofWatch.
Formal checking
Verified, corrected and revised the proof
- Checker
- Dawei Chen, Jingyin Huang, Yu Qiu and Fei Yu, authors
- Scope
- Appendix A's Yoshinaga-based proof of the two local arrangement obstructions
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The authors explain the sign-vector obstruction and retain the alternative proof as a complementary viewpoint after correcting it.
Correction and publication history
Provides a complementary proof of the local ingredient.
Read this published revision