Matthew Scherf has successfully verified the logical consistency of Śaṅkara’s Advaita-Vedānta metaphysical system. For that work he used the Lean 4 proof assistant, a functional programming language and theorem prover built for formalizing math and for formal verification. The Advaita-Vedānta was successfully verified with 0 logical inconsistencies. Here’s a nice presentation of that work.
Abstract. We present a first-order axiomatization of Advaita Vedānta metaphysics, formalized and verified in the Lean 4 proof assistant. The system comprises 69 primitive axioms organized into ten modules, capturing the core doctrines of non-dual Śaṅkara Vedānta including the identity of Ātman and Brahman, the three levels of reality, the theory of superimposition (adhyāsa), and the three-state analysis (avasthā-traya) from the Māṇḍūkya Upaniṣad. All proofs are machine-verified.
I just wonder if Buddhas Teachings could be axiomatized using high-order mathematical language and verified using Lean 4, just like they did with Advaita-Vedānta. If Buddha’s Teachings passes the test of logical consistency, this would be a great news for the Buddhist world.
Factor of faith in Buddhism:
Not logic but wholesome experience. So, no verification through logic but instead only through practice.
Moreover, range of Wisdom beyond logic.
Dhamma is for one who feels. Suffering isn’t logical category. As well entire experience. Certain descriptions are valid only within particular aspect of experience, so sometimes it is possible to encounter logically opposite descriptions, which most probably would be classified as lack of consistency, while it would be enough to order them hierarchically to see that inconsistency appears merely on verbal level.
A syllogism can be logically valid even if one or more of its premises are false. This logical validity, however, does not mean the conclusion(s) are true.
Secondly, some conclusions/knowledge(s) may be true but are beyond formal logic. For example, the knowledge of rebirth in Buddhism.
Reminds me of the well-known, yet still eyebrows-raising bit in AN3.65:
Please, Kālāmas, don’t go by oral transmission, don’t go by lineage, don’t go by testament, don’t go by canonical authority, don’t rely on logic, don’t rely on inference, don’t go by reasoned train of thought, don’t go by the acceptance of a view after deliberation, don’t go by the appearance of competence, and don’t think ‘The ascetic is our respected teacher.’ But when you know for yourselves: ‘These things are unskillful, blameworthy, criticized by sensible people, and when you undertake them, they lead to harm and suffering’, then you should give them up.
In other words, ‘practice/experience’ as a couple of people upstream commented.
Also, I notice that several of the views in DN1 were held by ascetics or brahmins who “speak of what they have worked out by logic”, yet the views contradict each other. Even if the Buddha’s teachings could be proven to be logically consistent using software, I personally guarantee that another religions apologist would be all like “nuh-uhh, our teachings are the best-est and here’s why…”.
Interesting. I’m looking forward to downloading the files and reviewing the code after I run it. I think proving that the canon is consistent would be a monumental and futile effort, but for those who believe the Atthakavagga and the Parayanavagga are the oldest Buddhist texts, there is hope.
Regardless of possible logical consistency of the Canon, those of us who practice Buddha’s methods know that they bring promised results. Practicing Buddha’s meditative practice of mettā-sādhana has reduced my suffering tremendously.
Maybe Buddha’s Teachings teaching was never meant to be a logically consistent system of thought. Buddha compared his teaching with a raft. It’s purpose is crossing the flood of suffering and reaching the far shore of peace, Nibbāna. One we get there, the need for the raft ceases and we can let go of the raft, the teachings.
Getting a kick out of all the responses poopoo’ing logic and consistency. Me thinks somehow some of the same commentators might howl with indignation at purported proofs that Buddhadhamma be illogical or inconsistent.
It might be an interesting project. I am opposed to the view that logic has no place in Buddhism, or have a lower value on it.
Any system of thought/practice/believe needs to be logical, this is the internal characteristic of the system where inside of it, assuming some things, we can build a logical system. At the same time, a logical system per se can mean nothing. You can have the most wrong view in the universe, your system could still be logical.
The importance is on the assumptions.
I think it makes more sense to understand that when the Buddha said to not rely on logic, it just means that only following something because is logical is a dangerous move.
However, I do believe the Buddha teachings will have a closed logical system. It is more curious than significant, though.
As a professional software engineer interested in formal verification, this does pique my interest a bit.
But I’d echo the other comments that pure logical self-consistency may not be altogether useful, or rather, skillful.
SN36.20 touches on seemingly contradictory explanations:
“Mendicants, in one explanation I’ve spoken of two feelings. In another explanation I’ve spoken of three feelings, or five, six, eighteen, thirty-six, or a hundred and eight feelings.
There might be a way to formalize such things (I’m not sure and am no proof engineering expert by any remote measure, especially not in Lean), but this is far from the only such sutta.
What set of suttas to consider would be another open question (the entirety of the Nikayas? more? less? what about the agamas?), as would how to formalize verse.
Rather than the goal being pure logical self-consistency, it may be more skillful to use such an analysis for other means. For example, which suttas are harder to understand, the percentage of inconsistency per sutta, possible assistance in dating texts and determining what may be ‘future additions’, etc.
Some of those goals already have existing forms of analysis, such as textual (style and word consistency) or stastical (e.g. word frequency). A logical analysis could be complementary to those, but in any case, I think the skillfullness of the task and goals are important to consider
Thanks for sharing the link. I think it would be worthwhile to attempt something similar for the Buddhist canon(s). The Buddha loved lists and lists of lists. Had he been instantiated in the 20th century, he would’ve relished programming in LISP, the great ancestor of all theorem-proving languages.
Some of the commentators have emphasized that there is no substitute for practice. I prefer practice as well, but surely, the jnani yogi cannot be denied liberation simply because they prefer reason over meditation. Had Nagarjuna not engaged in those great logical debates of his day, Buddh”ism” may not have survived on the subcontinent. Similarly, is Jay Garfield, who has done so much to explicate the Mūlamadhyamakakārikā any less of a Buddhist or farther removed from liberation than any meditator?
That said, for me the Buddha’s teachings often have the same feel as Plato’s dialogues. They are not so much logical statements as they are invitations to consider the questions at hand seriously. Drew Hyland’s “Why Plato Wrote Dialogues” makes the case that the dialogic form is an essential feature of Plato’s worldview and not simply an aesthetic container for certain logical arguments. Perhaps the same is true of the Buddha’s teachings. Viewed purely through the lens of formal logic, they may not seem very sound. But in a world overly-dependent on the Guru, the frequent invitations to disagree with the teacher must have been seen as a thoroughly radical move.
This is a fascinating exercise. But I do possess reservations about considering these results worthwhile in the service of cultivating a path to liberation.
Logical consistency or internal consistency of a tradition can inspire confidence to take on the path or training prescribed by the tradition. But beyond that it may not guarantee that that path prescribed by the training is practical or effective in achieving the goal!
Advaita Vedanta shares a lot of common ground with North Indian Buddhism of the time (7-8 century CE). So much so, that Ramanujan, the major figure in another later Vedanta tradition criticizes Advaita Vedanta and its main teacher Shankaracharya as crypto-buddhist. And he is not alone in that accusation.
As a EBT guided practitioner I have had delightful conversations with Advaita practitioners (including a very close friend) where we compare notes on liberation doctrines and find that dispassion and disillusionment with the material world is very much part of both traditions. I feel that there are considerable overlaps.
But I noticed some difficulties that two advaita practitioners I know, have in their lives. Owing to the internal consistency and logical appeal of their doctrine, they have cultivated dispassion and disillusionment with the material world intellectually. But they seem to be lacking in a clear antidote to this and wholesome source of pleasure, like the Jhānas, that can sustain them through the long spiritual training required. They agree theoretically on the benefits of Bhakthi or boundless love as a source of wholesome pleasure. But owing to either poor insistence or poor cultivation they seem to lack it. Both of my friends show a predilection to depression and despair.
I don’t wish to generalise based on a few conversations with two practitioners. But it made me reflect on how much practical insistence there is on wholesome pleasures, the bliss of renunciation and seclusion, the necessity of Jhānas there is in the Buddha Dhamma. And it brought me joy and confidence to my practice that the teachings are of such practical nature.
So logical consistency is interesting. But in terms of walking a path to liberation it may not be enough or necessary. Especially as other comments have pointed out - The Dhamma is for one who feels!
The first mathematics with logic formally verified with a computer–that would be, Godel’s incompleteness theorems. Somewhere I have a copy of a mathematics magazine with an article about it. Of course, Godel’s theorems were based on axioms of logic, a subject that can be readily translated into the language of computers.
Godel’s theorems tell us that if it’s complete, it’s inconsistent, whereas if it’s consistent, it’s incomplete. I like to think of that as the explanation for what Bhikku Bodhi described:
… not only are the texts themselves composed in a clipped laconic style that mocks our thirst for conceptual completeness, but their meaning often seems to rest upon a deep underlying groundwork of interconnected ideas that is nowhere stated baldly in a way that might guide interpretation … the nikāyas (EBT sermons) embed the basic principles of doctrine in a multitude of short, often elusive discourses that draw upon and allude to the underlying system without explicitly spelling it out. To determine the principles one has to extract them piecemeal, by considering in juxtaposition a wide assortment of texts.
(Bodhi, “Musīla and Nārada revisited: seeking the key to interpretation,” in (edd) Blackburn & Samuels, Approaching the Dhamma, Buddhist Texts and Practice in South and Southeast Asia, Pariyatti, 2003; parenthetical added)
Gautama chose to be incomplete, rather than inconsistent.
Modern people generally seem to have an intellectual inclination, and this can also be observed among Buddhists. However, I believe the more important point is that there is a significant difference in the nature of awakening itself. Advaita teachers tend to portray the world in a positive light, whereas Buddhism takes the opposite approach.
Is that so? In my conversation with my close friend who is an Advaita Vedanta practitioner, she really did seem to accept that the world is rather lackluster and not worth generating passion for; even went as far as agreeing that the only worthwhile pursuit that exists in this conditioned existence is the pursuit of the path out of this conditioned existence - to the unconditioned.
From this I inferred that there is an insistence of seeing the world in not too positive of a light. But I would not be surprised if there are teachers who teach the opposite as there is always some confusion within the massive body of Vedic and Hindu literature with a great deal of conflicting ideals being present together all the time.. it takes effort to even parse through and find consistent material, much less follow it.
This kind of work is interesting, but I think its significance is easy to overstate. What Lean shows is that a particular axiomatization doesn’t generate contradictions under a particular formal logic - that’s relative consistency, not some final verdict on a tradition. Gödel’s incompleteness theorems matter here: any sufficiently expressive system that’s consistent will necessarily be incomplete, so “0 inconsistencies” doesn’t mean the system is finished, exhaustive, or captures everything that matters.
You may reply that consistency is still important - and sure, it is - but consistency by itself is fairly cheap. You can almost always get it by restricting what you formalize, weakening axioms, or leaving hard things informal. What can’t be mechanically checked is whether the axiomatization actually reflects the tradition in a deep or adequate way.
In the Buddhist case there’s also an extra wrinkle. The Buddha often says different things to different people, depending on their dispositions, level of understanding, and existing views, all for the pragmatic purpose of helping them make progress toward the ending of dukkha. From that perspective, some apparent inconsistencies are not a bug but a feature. They reflect skillful means, not confusion.
And there’s a deeper reason inconsistencies aren’t especially scandalous here. The Buddha repeatedly points out that the deepest aspects of the Dhamma - nibbāna, emptiness, the unconditioned - cannot really be captured in words at all. Language operates at the level of conventional truth, not ultimate realization. So trying to force the Dhamma into a fully explicit, closed, axiomatized system may already miss something essential.
So yes, you could try to formalize parts of the Buddha’s teaching and check them in Lean - but passing a consistency check wouldn’t be “great news” in any deep sense. It would just tell us that one formal shadow of the Dhamma hangs together logically.
Well said. I think when spiritual practitioners follow a path predominantly guided by intellectual indulgence, there is a danger in overstating the importance of such analysis of logical cohesion or intellectual consistency that can be stated objectively. Because that is all an intellectual tradition provides. To practice confidently you need to have faith and belief in the system - an intellectual system can only engender confidence and faith through analysis of such objectively stated intellectual consistency.
I think confidence in the tradition or Dhamma is essential for doubt free progress - the Buddha Dhamma does this through various means that are not limited or reducible to intellectual means. The essentialness of Jhānas towards realization of the goal has been stated well in the EBT! I don’t see how the core of this experience can be captured or codified well through words, axioms or formulas. Also they make for such blissful and peaceful abiding - which is just a wonderful bonus.
