s/Coq/Rocq not found (Was: FYI: Peter Aczel Memorial Conference [10th September 2025])

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.

>

>

>