I'm reminded of Roger's Version by John Updike. I remember reading it and thinking "What the hell is wrong with people?"
-----Original Message----- From: Friam <[email protected]> On Behalf Of glen Sent: Sunday, August 31, 2025 8:09 AM To: FriAM <[email protected]> Subject: [FRIAM] adversarial slop 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/
smime.p7s
Description: S/MIME cryptographic signature
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. 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/
