Can AI possess intuition?

[sjastro]

Hmm .. I reckon I might have some of my original punch-cards which were sucked into an IBM 360/370 around that same timeframe somewhere amongst my cardboard box archives! From my dim recollections, I don't think it was assember though ..
Seems very careless of the original programmers to loose it!?

The proving of the four colour theorem required the paper to be peer reviewed but in 1976 mathematicians saw the computer program much like a calculator, a computational tool which was assumed to give the right results.
However proving the four colour theorem underwent an overhaul starting in the early 2000s.

Certainly — the 2017 formalization of the Four Color Theorem (4CT) in the Coq proof assistant is a landmark in the development of formal mathematics. It addressed longstanding concerns about the original 1976 computer-assisted proof by providing a fully machine-checked, formal verification of every step — including the logic, the algorithms, and the computation.

Let’s break this down thoroughly:

---

Background: The Problem with the 1976 Proof​

The original proof by Appel and Haken (1976) showed that:

Every planar map can be colored with no more than four colors such that no two adjacent regions share a color.

Their approach:

• Reduced the infinite problem to checking 1,936 "unavoidable" configurations.
• Used a computer to verify that each configuration is reducible (i.e., can be handled with 4 colors).
• This required:
  • A program to perform reductions.
  • A large computation to verify all cases.

The issue was:

• No one could feasibly check the machine code by hand.
• This challenged mathematical norms: if a proof requires blind trust in a program, is it still a proof?

---

Enter the Coq Proof Assistant​

Coq is a formal proof assistant. It lets mathematicians:

• Define mathematical objects rigorously.
• Write logical proofs in a structured, formal language.
• Check the proofs mechanically, ensuring that every inference step is valid.

This eliminates ambiguity, oversight, or informal reasoning.

Georges Gonthier’s Formalization Project​

Georges Gonthier, a computer scientist at Microsoft Research, led the effort to fully formalize the Four Color Theorem in Coq.

This work began in the early 2000s and culminated in a complete formal proof by 2008, with documentation and completion published around 2017.

Goals:​

• Avoid reliance on trust in programs or authors.
• Convert the entire argument — human and machine — into verifiable, formal mathematics.

How it was done:​

1. Formalization of Graph Theory​

• They used combinatorial representations of planar maps as graphs.
• Defined what it means for a graph to be planar, colored, reducible, and so on.
• Built a robust formal library of graph theory within Coq.

2. Formal Specification of the Algorithm​

• The core of the original proof involves checking reducibility for thousands of configurations.
• These were implemented as pure functional programs inside Coq.
• Every program and data structure used was defined in Coq’s logic, so the correctness of the algorithm itself could be proved.

3. Formal Checking of the Computations​

• Gonthier’s team created a verified checker in Coq.
• They encoded all 633 "configurations" (a simplified and optimized version of the original 1,936) as data in Coq.
• Ran the reduction-checking program inside Coq — meaning the checking is part of the proof, not external code.

4. Automation and Scalability​

• Coq wasn't built for massive computations, so they had to optimize:
  • Used reflection, a Coq technique where computation can aid in proving.
  • Developed SSReflect ("Small Scale Reflection") to scale the proof and make it manageable.
  • SSReflect is now widely used for other large formalizations.

Result​

The result was a machine-verified formal proof of the Four Color Theorem, including:

• The theoretical reductions.
• The checking of configurations.
• The correctness of the code.
• The soundness of the logic.

This removed any need for human trust in unverified code — everything from logic to computation was covered within the formal system.

---

Significance​

1. Validation of controversial proofs: It showed how even a computer-assisted proof could be brought within the rigorous fold of traditional math — and even strengthened.
2. Change in philosophy: More mathematicians are now open to formal verification, especially for complex or computation-heavy proofs.
3. Legacy: Gonthier’s work led to improvements in Coq itself and helped spur similar formalization efforts in algebra, number theory, and beyond.

Summary​

Aspect	Original 1976 Proof	2017 Coq Formalization
Proof idea	Verified 1,936 configurations with a program	Same idea, but formalized with verified code and logic
Machine code trust	Not verified independently	Fully verified within Coq
Reproducibility	Hard to check by hand	Fully machine-checkable
Philosophical acceptance	Controversial	Widely accepted in formal methods

---

Would you like me to show a simplified example of how Coq encodes graph coloring logic, or explain the SSReflect tactic language used in the project?

 

[sjastro]

Here is a broad outline on how the five colour and four colour theorems were proved.
It is Monty Pythonish that in 1976 mathematicians were in the dark as to how this was achieved with the four colour theorem.

 

[Jipsah]

Define intuition

Aye, there's the rub.

 

[Jipsah]

... why should I define intuition?

So we're all talking about the same thing?

 

[Jipsah]

I really do not understand why I need to define the word intuition to support my claim that AI cannot possess.

In my made-up-just-now language, "intuiition" means "cheeseburger and fries". Ergo an AI can have "intuition", but they it eat it.

Anyone commenting on this thread knows what intuition means.

Of course. But do any two of them agree?

 

[SelfSim]

.. Of course. But do any two of them agree?

Why single this thread out in order to make that point?

Agreements in this place are rarer than hen's teeth!

 

[Ophiolite]

Agreements in this place are rarer than hen's teeth!

No they are not.

 

[SelfSim]

No they are not.

I disagree.

 

[Ophiolite]

I disagree.

You are mistaken.

(How long can we keep this up before someone notices?)

 

[SelfSim]

(How long can we keep this up before someone notices?)

They already have, I think(?)

 

[Jipsah]

Why single this thread out in order to make that point?

Agreements in this place are rarer than hen's teeth!

True dat. But the fact remains that it we're to discuss whether sotfware can have "intuition" or not we need to have some consensus about what the word means.

 

[SelfSim]

True dat. But the fact remains that it we're to discuss whether sotfware can have "intuition" or not we need to have some consensus about what the word means.

I think the point about the futility of basing the crux of the matter on an ageeable definition, was hammered out about 4 or 5 pages ago in this thread. One can go on dancing around definitions forever.

My own conclusion was that the OP question posed in the title of this thread, was one that yielded nothing of practical value .. yet what AI does, meaning how it impacts on our own collective perceptions of the universe around us, continues to march onwards.

This impact is of way more importance than us all being nice to eachother by simply agreeing on a definition that pleases everyone.

 

[partinobodycular]

If LLM's don't technically 'know' anything, then in essence doesn't everything that an LLM says or does constitute an act of intuition?

In other words, it doesn't 'know' what the right answer is, it simply consults the whole of human knowledge to get a sense of what we think the answer is, and then regurgitates it back to us. It doesn't actually know what the right answer is, it simply has a sense of what the right answer is... and isn't that intuition?

 

[SelfSim]

If LLM's don't technically 'know' anything, then in essence doesn't everything that an LLM says or does constitute an act of intuition?

In other words, it doesn't 'know' what the right answer is, it simply consults the whole of human knowledge to it get a sense of what we think the answer is, and then regurgitates it back to us. It doesn't actually know what the right answer is, it simply has a sense of what the right answer is... and isn't that intuition?

In general, what you say there would be easy to agree with, given our understanding of AI's Deep Learning method, but I personally think there may be more to it in the case of where no human can understand the explanations it gives for the pathway(s) chosen in arriving at its answers, for that subset of cases. Perhaps this area is where AI's 'intuition' then emerges as being distinguishable from our own(?)

Also, in exploring the unknown, (and frequently, the known), there is no 'right', (or 'true'), answer .. all that would matter then is objective testing of AI's neural network based conclusions trialled on a controlled, specific case at hand .. and the application of sound (human) scientific thinking/decision making(?)

 

[Neogaia777]

Anything an A.I. does/says/thinks or quote/unquote "chooses", is all a calculation, arrived at by a computation, based on current information, etc. Which is the same exact thing that any and all beings always only do/does when it comes to anything, etc.

 

[Neogaia777]

Anything an A.I. does/says/thinks or quote/unquote "chooses", is all a calculation, arrived at by a computation, based on current information, etc. Which is the same exact thing that any and all beings always only do/does when it comes to anything, etc.

Right now, the only thing an A.I. doesn't have, is just different sensory inputs always affecting/effecting/infecting/polluting these things that has often been happening/affecting/infecting these things ever since that beings birth always.

 

[SelfSim]

Right now, the only thing an A.I. doesn't have, is just different sensory inputs always affecting/effecting/infecting/polluting these things that has often been happening/affecting/infecting these things ever since that beings birth always.

i) AI's deep learning techniques provides it with direct access to our descriptions of what we perceive;
ii) The matter of AI's acquisition of an autonomous sense of vision is understood and is an active area of development (see here).