Heyting algebras as subterminal lattices of elementary toposes

Free two-generator counterexample

Model / AI: ChatGPT 5.6 Sol

Ye and Xu state that the mathematical results were obtained with ChatGPT's help. They prove that the free Heyting algebra on two generators cannot occur as the subterminal lattice of an elementary topos, answering the question negatively.

Source read 2026-09-08. Read the abstract and AI-use statement in arXiv v1. No independent or formal check was found.

• Paper — Paper