Priority is not the claim here and is not needed. The core of the Nyāya Sūtra is placed around the 2nd century BCE and the redaction that survives is often put several centuries later; on either dating Aristotle's Organon is earlier, and the debate tradition Nyāya codifies is older than either text. What matters is that the two traditions are independent, and that Nyāya kept three things the Greek form set aside as redundant.
The Greek syllogism is premises and conclusion. Nyāya's inference has five members: the claim (pratijñā), the reason (hetu), the general rule together with an example (udāharaṇa), its application to the case (upanaya), and the conclusion (nigamana). The third member exists so that an argument establishes not only validity but factual anchoring — the rule must be shown holding somewhere, in a case a listener can check.
Nigrahasthāna — points of defeat — is one of the sixteen categories of the system, and hetvābhāsa names five ways a reason can merely appear to be one: inconclusive, contradictory, counterbalanced, unproved, and mistimed. A catalogued taxonomy of how argument fails, built into the framework rather than accumulated by accident afterwards.
The four pramāṇa — perception, inference, comparison, testimony — are kinds of knowing, not degrees of confidence, and testimony is admitted as its own bounded source with its own conditions rather than smuggled in as weak perception. A machine record and a page's assertion are different kinds of warrant, not the same warrant at two strengths.
The convergence is the first half of the point: two traditions, out of contact, both isolate inference as a thing with parts, both name the ways a reason fails, both build an apparatus for adjudicating a claim in public. The second half is that they then developed different axes, and the asymmetry is not a matter of one side being cleverer.
Where the Greek line went further. Aristotle's schematic letters — A belongs to all B — abstract form from content, and that single move is what eventually made logic mechanisable. The Stoics added propositional connectives and their inference schemes. Nyāya's inference deliberately stays attached to content: the udāharaṇa is required because content matters, which is a strength for adjudication and an obstacle to formalisation. The line that runs to Frege, to Mathlib and to a proof-assistant kernel is the Greek one, and it is not an accident that it is. Reading
Where Nyāya went further. On the question of when instances license a general claim, Greek epagōgē is thin and the problem stays open until Sextus and then Hume; Nyāya built vyāpti into a theory, with upādhi — the limiting condition that silently defeats a concomitance — as a named object to be searched for before the inference is granted. And the syllogistic stood substantially unchanged from Aristotle to the nineteenth century, while the Indian tradition kept developing: Gaṅgeśa's Tattvacintāmaṇi and the Navya-Nyāya after him built a technical language for relations and for negation of relational complexes that Ingalls and Matilal both argued is more expressive than the syllogism ever became.
A proof-assistant kernel is form abstracted from content, executed perfectly. The failures that matter in practice live on the other axis: whether the theorem says what was meant, whether a name claims more than its proof, whether a sweep holding one parameter fixed has established a concomitance or merely confirmed itself, whether “machine-checked” on a page and a gate record are the same kind of warrant. Those are upādhi questions and pramāṇa questions. The compiler cannot be blamed for being silent about them; it descends from the tradition that set them aside in order to become a compiler.
Neither system was copied from the other and neither was learned. Each was derived, from the same first principles, by people addressing the same problem: how does a claim earn assent, and how does it fail.
The differences are the evidence. Transmission produces the same decomposition in local vocabulary. What is actually there is two systems that agree completely on what the problem is — inference has parts, reasons fail in nameable ways, warrant comes in kinds — and disagree on how to cut it: five members against two premises, an epistemology of pramāṇa against a theory of formal validity, the worked instance kept against the worked instance discarded. Copying does not produce disagreement at the joints while producing agreement about where the joints are. Inference
Which changes what the observation is worth. A parallel is a curiosity. Two independent derivations mean the apparatus is a property of the problem — of inference held up to scrutiny — and not of a culture, a language, or a period.
In September 2026 this project derived the same structure again, from a night of failed proof-assistant runs and nothing else. Nobody consulted Akṣapāda. From a report that named a frozen deposit as if it were a live file, a parser that dropped a declaration whose name ended in a prime, a wrapped axiom list hiding an admitted theorem, and a sweep that varied one axis of a two-axis claim, came three rules: keep the worked instance with the rule; name the ways a reason fails; distinguish kinds of warrant.
Three of Nyāya's central commitments, reached backwards from broken output. The standing objection to any historical parallel is that transmission cannot be excluded. Here it can: the derivation is timestamped commit by commit in docs/audit-log.md and can be audited by anyone who doubts it.
The practical consequence is not to admire the parallel but to stop deriving the apparatus from failures. Vyāpti — invariable concomitance — and upādhi are precisely the question of when a sweep over instances licenses a general claim. In this project's own instrument that question is a manual step with no tool behind it. That work has been done, in detail, for a very long time. Reading it is cheaper than rediscovering it a fourth time. Open