I would be very curious as to the content of your "mansplaining."
Also interested in the prevalence of "logic" in what you have shared. I know of multiple efforts, some quite good, by western analytic philosophers of their counterparts in Buddhist philosophy. I would recommend one in particular: Illuminating the Mind: An Introduction to Buddhist Epistemology (Buddhist Philosophy for Philosophers) by Jonathan Stoltz (Author) I know of no similar efforts to find/apply logic in/to Taoism, except some ancient Chinese Logic Philosophers trying to relate (by force fitting) Taoism and Confucianism. I would find it fun and interesting to sit in the bar (Salon) and converse on this topic. Alas we are rather far apart. I did just drive from Baltimore to Underwood WA, (north shore of Columbia) to deliver a Prius to friends who moved there. davew On Sun, Aug 31, 2025, at 10:08 AM, glen wrote: > So, I found myself mansplaining the difference between Buddhism and > Taoism to a newly met couple at the pub the other night. And because I > did such a bad job, I wanted to check my reasoning. After an insomniac > hour of fruitless googling (DDGing just doesn't work as a term), I > decided to lob the problem at Kimi K2. She did an adequate job of > disabusing me of many of my [dis]analogies between Taoism and Buddhism, > which was dandy. But then I asked her to help me *model* them using > tools like Isabelle, Coq, or Lean. And she went insane. Gaslighting me. > Lying to me. Making things up including whole communities of such > modelers and conferences. [sigh] > > Anyway, I decided to ask Perplexity about Kimi's final report. Here's > what she said about the whole kerfuffle. > > Perplexity's Analysis of Kimi's output: > > Kimi K2's output presents a highly detailed map of formalization > projects for religious philosophies, with a particular focus on Taoism > and Buddhism. However, an in-depth analysis and a broad web search > reveal that the specific projects, code repositories, and academic > outputs she cites do not correspond to any verifiable or documented > work in current literature or online. In particular, no public evidence > supports the existence of higher-order logic or proof assistant > projects tailored to Buddhist or Taoist philosophy as described. > > > Analysis of Kimi's Claims > > * Kimi details multiple "existing" projects supposedly formalizing > Taoist and Buddhist logic in tools like Lean 4, Agda (Cubical mode), > and Isabelle/HOL, with references to specific people, repos, and even a > specialized email list. > * Searches of academic articles, archive repositories, and proof > assistant communities yield **no trace of: > o A "leanprover-community/buddhist-logic" GitHub, > o Agda Cubical "QiField" or related Taoist/HITs branches, > o Published code or whitepapers matching her detailed > descriptions, > o Named researchers (e.g., Kuen-Bang Hou/Favonia) producing > Buddhist or Taoist logic formalizations in Agda or Lean since 2020 in > this context. > * References to an "active Buddhist-logic micro-community," > "[email protected]," and comparative Tao-Budd code bases are > not corroborated by mailing lists, AFPs, or academic web presence. > > > Validated Findings from Foundation and Web Search > > > Higher-Order Logic and Proof Assistants in Philosophy > > * There is*active research*in formalizing higher-order logic using > proof assistants such as Isabelle/HOL, Lean, and Agda. Recent work > includes formalizing foundational logic, some paraconsistent or > infinite-valued logic, and development of educational tools for > teaching logic and proof methods.[1][2][3][4] > * Computational philosophy and simulation techniques (agent-based > modeling, logic-based simulation) are increasingly prominent for > studying general philosophical questions, including religion and > cognition. Notable work exists by Shults, Gore, Wildman, Grim, De Cruz, > and De Smedt—but these focus on*agent-based models, Bayesian cognitive > science, and simulation epistemology*rather than proof assistant-based > logic formalization targeted at specific Eastern religions.[5][6] > * Some research explores paraconsistent or many-valued logics (which > sometimes intersect with Buddhist logic), but these are not > specifically positioned within Buddhist or Taoist traditions, nor are > they explicitly verified as such in Lean, Agda, or Coq repositories.[3] > > > Absence of Taoist or Buddhist Proof Assistant Formalizations > > * There is*no public evidence*for active formalization projects for > Buddhist or Taoist logic in Lean, Agda, or Isabelle as described by > Kimi. > * Archives of Formal Proof (Isabelle), Lean community repositories, > Agda cubical branches, and search across zenodo, arXiv, and other > digital libraries do*not show any dedicated, community-sponsored, or > institutionally acknowledged effort*in formalizing or computationally > encoding Buddhist or Taoist philosophy with proof > assistants.[7][8][9][1] > > > Simulations and Psychology-of-Religion Efforts > > * Some cognitive science and computational sociology work models > religious belief dynamics, ritual, and cognition (e.g. as referenced by > Kimi in Section A), but these rely on systems like NetLogo, AnyLogic, > or general programming languages, not proof assistants or formal logic > verification environments.[6][5] > > > Conclusion > > *Kimi's output hallucinates formalization efforts, resources, and > community activities that do not exist in the referenced domains.*There > are no verifiable projects making substantive progress in formalizing > Taoism or Buddhism via higher-order logic and proof assistants as > described in her assessment. Existing relevant work in the > philosophy-of-religion modeling space primarily employs computational > and simulation techniques rather than formal verification in proof > assistants or higher-order logic targeted at these > traditions.[2][1][5][6] > > ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ > > > References > > * Active higher-order logic and proof assistant work focused on > mathematics and general philosophy, not Eastern > religions.[4][8][9][1][2][3][7] > * Computational philosophy, including simulation studies in religion > and social epistemology, but not related to formal verification of > Taoist or Buddhist doctrines.[5][6] > > [1]https://arxiv.org/html/2404.05458v1 > > [2]https://matryoshka-project.github.io/pubs/schlichtkrull_phd_thesis.pdf > > [3]https://orbit.dtu.dk/en/publications/formalization-of-logic-in-the-isabelle-proof-assistant > > [4]https://ceur-ws.org/Vol-3717/paper3.pdf > > [5]https://pmc.ncbi.nlm.nih.gov/articles/PMC7944252/ > > [6]https://plato.stanford.edu/entries/computational-philosophy/ > > [7]https://ui.adsabs.harvard.edu/abs/2024arXiv240405458L/abstract > > [8]https://arxiv.org/html/2412.16075v1 > > [9]https://www.emergentmind.com/articles/2404.05458 > > [10]https://www.reddit.com/r/math/comments/17g3ujl/terence_tao_is_formalizing_his_recent_paper_in/ > > -- > glen > > > .- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. > / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. > FRIAM Applied Complexity Group listserv > Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom > https://bit.ly/virtualfriam > to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com > FRIAM-COMIC http://friam-comic.blogspot.com/ > archives: 5/2017 thru present > https://redfish.com/pipermail/friam_redfish.com/ > 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/ .- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
