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/
