Path: nntp.eternal-september.org!news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: s/Coq/Rocq not found (Was: FYI: Peter Aczel Memorial Conference [10th
 September 2025])
Date: Thu, 17 Jul 2025 23:16:19 +0200
Message-ID: <105bp71$2cikh$1@solani.org>
References: <1056abq$2ar22$4@solani.org> <105ahlr$2boci$2@solani.org>
 <105aics$2botd$1@solani.org> <105aqk0$2btjj$2@solani.org>
 <105arsd$2bue0$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Thu, 17 Jul 2025 21:16:17 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="2509457"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101
 Firefox/128.0 SeaMonkey/2.53.21
Cancel-Lock: sha1:0sk1dggmVxLzSB+33TShfqBLsDI=
In-Reply-To: <105arsd$2bue0$1@solani.org>
X-User-ID: eJwFwQkBwDAIA0BLfCFUzmjBv4TdwVPzMhIZWKyTBWkeU6mPq/WMNi5R/dCzknEWbqeV0nVf7xRv+qTrfj8rZhUR

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
========== REMAINDER OF ARTICLE TRUNCATED ==========