$ whoami
Carlo Perassi
The personal site answers "who is Carlo?". This site answers "what is Carlo building, testing, reading, or formalizing on GitHub?". It is intentionally a map, not a portfolio brochure: many entries are experiments, notebooks, drafts, or narrow tools.
ls ./
- projects/ — a curated atlas of public GitHub work
- blog/ — a public log of activity across my repositories
- writing/ — working drafts, article PDFs, and book material
- cv/ — a short curriculum vitae
ls _posts/ | head -3
sharp-symmetry-bounds-lean registered in the Palomar registry: PALOMAR-2026-09-18-000007
carlok/sharp-symmetry-bounds-lean
is now a registered entry in the Palomar registry —
PALOMAR-2026-09-18-000007, version 1,
status registered, trust level high, on the source of
commit ced9fe2
(the record’s own copy of the entry is
here).
This is the first third-party verification of one of these formalizations, and
what the registry actually did is the news: it rebuilt the project in a sandbox
from the pinned dependencies (Lean v4.32.0), exported the proof terms with
lean4export and replayed them on nanoda, an independent kernel
implementation rather than the author’s own build, then used the
Comparator
to check that Solution.lean proves the Challenge.lean statements — five
theorems of SharpSymmetryBounds — using only propext, Quot.sound and
Classical.choice, verified at 2026-09-18T13:50:47Z.
diaz-modulus-lean and prove2me-logs: the four exponentials theorem in transcendence degree one is proved
The 1973 construction whose four children
began to close in
diaz-modulus-lean is finished, and
with it the four exponentials theorem in transcendence degree one. The norm child
went first: FourExp.norm_to_polynomial_alg is proved
(a38d9db) by linear
algebra rather than the paper’s conjugates — the value is presented as
Π ∈ ℤ[X][Y] reduced modulo the monic Q, P = det M is the determinant of
multiplication by Π in the basis 1, Y, …, Y^(d−1), non-vanishing comes from a
kernel vector that would contradict the minimality of Q, and smallness from the
adjugate identity M·adj M = (det M)I. That made the core,
FourExp.construction_core_1973, a Proved node by cascade.
caciarabot: the digest stops posting links it cannot read
The digest in caciarabot now skips
candidate links whose target page is in another language
(7fd451b), because
GitHub trending routinely surfaces repositories documented entirely in Chinese —
two of the fifty candidates in that day’s live fetch were exactly that, and
posting one of them as the link of the day wastes the slot. The check runs in two
stages, cheapest first: the pool is filtered on the title and description the
source already returned, no extra request; only the picked candidate is fetched
and checked, because verifying fifty to post one would be fifty requests a day,
and a rejection drops that link and draws again, up to five times. For a GitHub
repo the check reads the raw README rather than the repo page, since github.com
serves <html lang="en"> on every page it renders, including for repos written
entirely in Chinese; elsewhere the declared lang decides, falling back to an
English-stopword ratio over the visible text. Two deliberate non-rejections:
Latin-script languages pass the metadata stage (ten words of French cannot be told
from English reliably), and a page yielding no usable evidence is accepted rather
than quietly thinning the pool — and Greek is left out of the non-Latin script set
on purpose, since a lone alpha here is more likely to be mathematics than prose.