- Author
- Posted by hotrollhottakes.bsky.social, with replies from many commenters
- Published
- 3 August 2026
- Kind
- Bluesky thread linking a Substack essay and a Lean proof
- Original
- bsky.app/profile/hotrollhottakes.bsky.social/post/3ms6yhtyp2t2g
- Subject
- Occult, myth and religion
What it is
The poster at hotrollhottakes.bsky.social announces an essay on Substack. Its title is The Internal Logic of Buddhism Is Verifiably Correct. The poster later links a Lean 4 repository. It holds a Lean formalization of a paper on emptiness in modal logic.
What it says
- The opening post says Nagarjuna's reasoning has an internal logical structure that is machine-checkably coherent.
- The poster says the Lean proof is linked only at the end of the essay.
- In a reply, the poster says the results strongly imply the Resolute reading of Wittgenstein.
- Stella Athena asks if the work proves consistency, not correctness. The poster replies that consistency suffices to refute foundationalist ideas of intrinsic necessity.
- Another commenter says validity is a low bar. The commenter says a false premise can sit under a valid argument.
- Other replies offer parallels to Ogyu Sorai, Pyrrhonism and Godel, Escher, Bach. The poster says the result is not a strict validity proof.
What evidence it gives
The thread offers claims and links. The proof lives in the linked Lean repository. The linked essay and the repository were not read for this page.
Interests and limits
The poster presents the thread as the poster's own result. The essay, the paper and the Lean code were not read. The claims were not checked. Images in the replies were not viewed, though their alt text was read. The thread was read in full. The linked essay, paper and Lean repository were not read.