Subject: Reality of Proof Assistants / Coding [Luhmans Zettelkasten] (Re: Free Speech for (my) Robots)
Hi,
The main problem, when it comes to proof writing
with proof assistants. Its just like code writing.
Basically fire and forget, either you document or
you dont document, but you want to flush your
brain and move on to other problems. So most
of the Isabelle/HOL proofs are large essays
written over many months, and the author has
disembodied himself from the topics. So these
proofs never satisfy the cringe Terrence Tao,
requirement which is copied from a PhD
examination playbook:
"My own suggested rule of thumb: if the authors
cannot convincingly demonstrate that they are able
to give a clear, expert-level talk on their results, one
that is correct and properly attributed, then the result
should not be published. A proof that no human
can properly explain should be viewed as incomplete,
even if it has been formally verified."
https://arxiv.org/abs/2608.16753
What you can try is a kind of V-model disciplin,
and write done higher level specs as well.
But sometimes traceability between layers is
quite brittle, you will do it informally. The cringe
Terrence Tao requirement wouldn't work either
for the books that Terrence Tao wrote, or any
other "tome" by any other author on this planet.
In case of Terrence Tao it wont work, because he
Terrence Tao maybe dead tomorrow, or because
I doubt that he remembers all his books he wrote,
and all the spontaneous rationals, in his books.
Its allways fire and forget, so that others or yourself
can pick it up, in case they/you need something, and read it.
Bye
The fire and forget and externalization of knowledge
is possibly best explained in Luhmans Zettelkasten:
https://niklas-luhmann-archiv.de/nachlass/zettelkasten
Mild Shock schrieb:
Hi,
So the Chinese Room Argument, whether
the Chinese in the room only follows rules
or not, is not relevant now.
What we do want, is no Chinese in the Room
anymore. Is it really Chinese? Basically the
stupid Academic Elite with its publication
Monopole, and their "Review Processes"
which is totally fake, are frightened to death.
They put a lot of effort in creating a new
Something AI Should Tell You ?
The Case for Labelling Synthetic Content https://onlinelibrary.wiley.com/doi/full/10.1111/japp.12758
regulatory protectionism disguised as ethics.
Its just another "burning of (my) books"
create on my Budget AI Laptop:
BAP - Kristallnaach [Live 1999]
https://www.youtube.com/watch?v=K-ZCGVb26pA
So fuck you Terrence Tao!
Bye
Mild Shock schrieb:
Hi,
Since for MIME type "text/*":
Within four hours of Anthropic confirming that
Claude models would globally embed invisible,
machine-readable watermarks into any AI-generated
content, developer Guillaume Meyer had
published his override
https://www.wired.com/story/coders-say-they-already-found-workarounds-to-claudes-invisible-watermarks/
BTW, I increase my "Convincingness" of my content,
abviously cocreated with AI, since I cannot
live anymore without AI, by removing the tag:
User-agent: AutonomousAIEventHorizon
Have Fun!
Bye
The AI Event Horizon in Software Development
https://www.northcode.fi/article/the-ai-event-horizon
Maria Sophia schrieb:
Somewhat related to AI watermarking is this recent article in the
news.
˙˙ *What does it mean to put a watermark on AI text?*
<https://edition.cnn.com/2026/08/20/us/word-of-the-week-ai-watermark-cec>
Which references:
˙˙ *How Claude's text watermark works*
˙˙ <https://www.anthropic.com/news/claude-text-watermark>
˙˙ *How AI text watermarking works*
˙˙ <https://declaude.org/watermarking/>
Where apparently there is an EU law which requires watermarking...
<https://edition.cnn.com/2026/08/11/business/video/invisible-watermarks-coming-claudes-ai-written-text-digvid-vrtc>
There's also this referenced, but it's behind a paywall.
˙˙ *Technology that can detect text written by AI with 99.9% certainty*
<https://www.wsj.com/tech/ai/openai-tool-chatgpt-cheating-writing-135b755a> >>
Mild Shock schrieb:
Hi,
The Armer paper gets geopolitical in the end
chapters. But today you could pivot russia for
china, and you would get a nice piece of work.
But who is the Chinese Lenin, that allows
even rocks and stones to participate in
the class struggle?
˙˙"Finally, it is particularly necessary to
emphasize the importance of the work of Lenin
who in elaborating on the ideas of Marx and
Engels, developed a materialistic theory of
consciousness as a reflection of activity.
Attention should also be given to the Lenistic
statement of the fact that non-living matter
may also possess this property of reflection."
- Paul Armer, Page 22
Bye
Jens Kallup schrieb:
Es ist schlimm, das man in der modernen Zeit
trotz KI immer noch von dem spricht, was die
Welt anscheinend antreibt: GELD.
Wer Geld hat, hat Macht, kann Wissen einkaufen -
was ist mit den Rest ? Die kleinen haben kein Geld,
Amerika ist pleite und Deutschland hat nun wieder
eine neue Steuer - Kinderfonds, 10 Euro monatlich,
bis 18, angelegt fr den Staat Deutschland.
Mild Shock schrieb:
Hi,
How it started:
Speed
^
| * Machine
|˙ (1963)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
How its going?
Speed
^
| * Machine˙˙ * Machine
|˙ (1963)˙˙˙˙˙˙ (2026)
|
|
|˙˙˙˙˙˙˙˙˙˙˙˙ * Man
+--------------------->
Sophistication
Bye
ATTITUDES TOWARD INTELLIGENT MACHINES
Paul Armer
RAND Corporation
in
BIONICS SYMPOSIUM 1960
LIVING PROTOTYPES - THE KEY TO NEW TECHNOLOGY
https://books.google.ch/books?id=1ZMeAAAAMAAJ&pg=PA13
Stefan Ram schrieb:
˙˙˙ In "Mathematics in the Age OF AI" (2026-08-17) macht Terence
˙˙˙ Tao sich auf zirka 11 Seiten Gedanke darber, in welcher Form
˙˙˙ KI-Systeme von ihnen gefundene Erkenntnisse bereitstellen und
˙˙˙ wie diese in das mathematische Wissen integriert werden sollten. >>>>
Mild Shock schrieb:
Hi,
I even don't remember exactly why I landed
in comp.theory. A yes, because Rossy Boy,
was hooked on SIMD and didn't understand Hack.
But the Hack work, rather belongs to my
Alma Mater Zurich and my personal heros, Gutnecht
and Wirth, who wrote a one pass Modula
compiler during some christmas holidays,
back then when I was student. Not sure
whether the Ljubljana School can do that,
when I read this here:
Finite Algebraic Effects as dicts and such
https://www.philipzucker.com/bdd_term_alg_effects/
I only find gibberish like:
- ?Data? is somehow less mysterious to me
˙˙ than ?computation?.˙ [..] I don?t even
˙˙ know what ?computation? really is
- In temporal logic, there is a logic CTL
˙˙ which talks about computation trees.
- Algerbaic (LoL) effects is almost a complete
˙˙ hackery abuse of the notion of arity
˙˙ and that?s neat.
- Then there are 10^10 etc vectors which
˙˙ show up if you discretize 3d/4d space. [..]
˙˙ or reinforcement learning.
- Etc..
WTF is this guy smoking? I mean he even
doesn't uses math notation, only posts
Python code fragments
go go,
possibly a Python brain damage.
But still less sever than Rossy Boys.
Bye
Ross Finlayson schrieb:
Hello, here I'll post some design notes and a panel discussion
with some
chat-bots about making some sense of the "vector-wide scalar word" >>>>>> and "character machines", on commodity hardware about ubiquitous
operations.
It's considered at least tangentially relevant to comp.lang.c and
comp.lang.c++ because for example text is ubiquitous and the targets >>>>>> would be low-level, while the higher-level languages would have a
same sort of patternry, and for example that libc and cstdlib are
standard, and as with regards to POSIX and Unicode and so on.
Please feel free to excuse or ignore, or comment as freely.
Thanks for reading.
--- PyGate Linux v1.5.19
* Origin: Dragon's Lair, PyGate NNTP<>Fido Gate (3:633/10)