Wonder Years are Over: Next Step Mars (Re: s/Coq/Rocq not found)

So, we had the formal revolution:
Frege (1879): Predicate logic formalized
Peano (1889): Axioms of arithmetic
Hilbert (1899–1930): Formal axiomatic method, Hilbert's Program
Zermelo (1908): Axiomatic set theory (ZF, later ZFC)
Gödel (1931): Incompleteness theorems end Hilbert’s
    dream of a complete formal system
Then the machanized formal revolution:
Automath (1967): The first real proof assistant,
laying the conceptual groundwork.
Mizar (1970s–1980s): Building a readable,
structured formal language and large libraries.
Isabelle (1980s): Developing a generic proof framework, making formalization more flexible.
Coq (early 1990s): Fully fledged dependent type theory and tactic language emerge.
HOL family (1980s–2000s): Focus on classical higher-order logic with applications in hardware/software verification.
Lean + mathlib (late 2010s): Community-driven scaling,
large libraries, easier onboarding.
So we practically landed on the moon.
Next steps:
- Mars Orbit (Now–2030), AI-augmented theorem proving.
- Mars Surface — AGI-Based Proving (2030s?)
- Mars Camp - The Hub of Next-Gen Mathematics and Reasoning
quantum computers, distributed supercomputers, and even alien intelligences (hypothetically)
Mild Shock schrieb:

Hi,
 I am trying to verify my hypothesis
that Rocq is a dead horse. Dead
horses can come in different forms,
 for example a project that just
imitates what was already done by
the precursor, is most likely a
 Dead horse. For example MetaRocq,
verifying a logic framework inside
some strong enough set theory,
 is not novell. Maybe they get more
out of doing MetaRocq:
 MetaRocq is a project formalizing Rocq in Rocq
https://github.com/MetaRocq/metarocq#papers
 #50 Nicolas Tabareau
https://www.youtube.com/watch?v=8kwe24gvigk
 Bye
 Mild Shock schrieb:

Hi,
>
Ok I have to correct "Rational Term" was less
common, what was more in use "Rational Trees",
but they might have also talked about finitely
>
represented infinite tree. Rational trees itself
probably an echo from Dmitry Mirimanoffs
(1861–1945) “extraordinaire” sets.
>
Dmitry Semionovitch Mirimanoff (Russian:
Дми́трий Семёнович Мирима́нов; 13 September 1861,
Pereslavl-Zalessky, Russia – 5 January 1945, Geneva,
Switzerland) was a member of the Moscow Mathematical
Society in 1897.[1] And later became a doctor of
mathematical sciences in 1900, in Geneva, and
taught at the universities of Geneva and Lausanne.
https://en.wikipedia.org/wiki/Dmitry_Mirimanoff
>
This year we can again celebrate another researcher,
who died in 2023, Peter Aczel R.I.P., who made
as well some thoughtful deviance from orthodoxy.
>
Peter Aczel Memorial Conference on 10th September 2025.
Logic Colloquium will take place at the University
of Manchester  (UK) from 11th to 12th September 2025
https://sites.google.com/view/blc2025/home
>
Have Fun!
>
Bye
>
Mild Shock schrieb:

Hi,
>
An example of human intelligence, is of course the
name "Rational Term" for cyclic terms set forth by
Alain Colmerauer. Since it plays with "Rational Numbers".
>
A subset of cyclic terms can indeed represent
rational numbers, and they give a nice counter
example to transitivity:
>
?- problem(X,Y,Z).
X = _S1-7-9-1, % where
     _S1 = _S1-6-8-0-6-2-8,
Y = _S2-1-6-1-5-4-6-1, % where
     _S2 = _S2-0-9-2,
Z = _S3-3-0, % where
     _S3 = _S3-8-1
>
The Fuzzer 2 from 2025 does just what I did in 2023,
expanding rational numbers into rational terms:
>
% fuzzy(-Term)
fuzzy(X) :-
    random_between(1,100,A),
    random_between(1,100,B),
    random_between(1,10,M),
    fuzzy_chunk(M,A,B,C,X,Y),
    random_between(1,10,L),
    fuzzy_chunk(L,C,B,_,Y,Z),
    Z = Y.
>
% fuzzy_chunk(+Integer,+Integer,+Integer,-Integer,+Term,-Term)
fuzzy_chunk(0, A, _, A, X, X) :- !.
fuzzy_chunk(N, A, B, C, Y-D, X) :-
    M is N-1,
    D is A // B,
    H is 10*(A - B*D),
    fuzzy_chunk(M, H, B, C, Y, X).
>
Bye
>
>
Mild Shock schrieb:

Hi,
>
Rota often celebrated symbolic, analogical, and
conceptual understanding over brute calculation.
This philosophy has come full circle in modern AI:
>
- Large Language Models (LLMs) like GPT-4 don't
   just store facts — they recognize patterns,
   make analogies, and generate new structures
   from old ones.
>
- Rota’s work in combinatorics, symbolic logic, and
   operator theory is essentially pattern-based
   manipulation — exactly the kind of reasoning LLMs
   aim to emulate at scale.
>
Rota had a clear aesthetic. He valued clean formalisms,
symbolic beauty, and well-defined structures. Rota wanted
mathematics to mean something — to be not just correct,
but intelligible and expressive.
>
In contrast, modern AI (especially LLMs like GPT) thrives
on the messy, including: Noisy data , Inconsistency ,
Uncertainty, Contradiction. AI engineers today are mining
meaning from noise.
>
What counts as “structure” is often just the best
pragmatic/effective description available at that moment.
>
Bye
>
Mild Shock schrieb:

Hi,
>
Spotting Trojan Horses is a nice example
of creativity that also needs ground truth.
Gian-Carlo Rota was phamous for this truth:
>
"The lack of understanding of the simplest
facts of mathematics among philosophers
is appalling."
>
You can extend it to GitHub acrobats,
paper mill balerinas and internet trolls.
But mathematics itself had a hard time,
>
allowing other objects than numbers:
>
- Blissard's symbolic method
   He was primarily an applied mathematician and
   school inspector. His symbolic method was a way
   to represent and manipulate sequences algebraically
   using formal symbols.
>
- Gian-Carlo Rota (in the 1970s)
   Gian-Carlo Rota (in the 1970s) gave Blissard’s
   symbolic method a rigorous algebraic foundation. Rota
   admired the symbolic reasoning of 19th-century mathematicians
   and often described it as having a “magical” or “mystical”
   elegance — again hinting at interpretive, almost poetic, qualities.
>
- Umbral calculus
   Modern formalization of this method, often involving
   linear operators and algebraic structures. "Umbral"
   means “shadow” — the power-like expressions are
   symbolic shadows of actual algebra.
>
Bye
>
>
Mild Shock schrieb:

Henri Poincaré believed that mathematical
and scientific creativity came from a deep,
unconscious intuition that could not be
>
captured by mechanical reasoning or formal
systems. He famously wrote about how insights
came not from plodding logic but from sudden
>
illuminations — leaps of creative synthesis.
>
But now we have generative AI — models like GPT — that:
>
- produce poetry, proofs, stories, and code,
>
- combine ideas in novel ways,
>
- and do so by processing patterns in massive
    datasets, without conscious understanding.
>
And that does seem to contradict Poincaré's belief
that true invention cannot come from automation.

>

>

>

>