Human intelligence is limitless (Theorems 3.3 and 3.4)

Disproved

CogCons.human_intelligence_limitless

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

consequence-operatorlogictopology

Let $(C, \mathrm{Cn})$ be a cognitive-consequence space with cognitive-consequence topology $\tau$ . Then there is a mental representation lying in no CWO set, and there is a mental representation lying in some CWO set:

\Bigl(\exists f \in C\ \forall A \in \tau:\ f \notin A\Bigr)\ \wedge\ \Bigl(\exists f \in C\ \exists A \in \tau:\ f \in A\Bigr).

The paper concludes from these two theorems that human intelligence is limitless.

Preamble

import Mathlib
import Definitions.Def_CogCons_consequence_space

open CogCons.CognitiveConsequenceSpace

Formal statement

namespace CogCons

theorem human_intelligence_limitless {C : Type*} (S : CognitiveConsequenceSpace C) :
    (∃ f : C, ∀ A : Set C, S.IsCWO A → f ∉ A) ∧
    (∃ f : C, ∃ A : Set C, S.IsCWO A ∧ f ∈ A) := by sorry

end CogCons

Source

S. Acharjee and U. Gogoi, *The limit of human intelligence*, arXiv:2310.10792v2 [math.GM] (2023), https://arxiv.org/abs/2310.10792, Theorems 3.3 and 3.4 (p. 7); conclusion stated on pp. 22–23

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements, not by an independent auditor working blind from the code alone. The author knew the intended meaning while writing it, so it may read that intent into the code. Do not treat it as independent verification; compare the Lean code against the source directly.

For every type $C$ and every cognitive-consequence space $S$ on $C$ — that is, a map $\mathrm{Cn}$ from subsets of $C$ to subsets of $C$ and a binary operation $\Rightarrow$ on $C$ such that $C$ is countable, $A \subseteq \mathrm{Cn}(A)$ , $\mathrm{Cn}$ is monotone and idempotent, every $x \in \mathrm{Cn}(A)$ lies in $\mathrm{Cn}(B)$ for some finite $B \subseteq A$ , $y \in \mathrm{Cn}(A \cup \{x\})$ implies $(x \Rightarrow y) \in \mathrm{Cn}(A)$ , and $\mathrm{Cn}(\varnothing)$ is nonempty — both of the following hold:

there is $f \in C$ such that for every $A \subseteq C$ with $\mathrm{Cn}(C \setminus A) = C \setminus A$ , $f \notin A$ ;
there are $f \in C$ and $A \subseteq C$ with $\mathrm{Cn}(C \setminus A) = C \setminus A$ and $f \in A$ .

No hypothesis beyond the structure axioms is assumed. $C$ may be any countable type, including a one-element type; the axioms allow $\mathrm{Cn}(A) = C$ for all $A$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph