#semiautomatic — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #semiautomatic, aggregated by home.social.
-
In mid-February, I set up a small informal seminar in my department, the "Semiautomatic Lean Working Group", to actively test out new LLM-based Leaning capabilities of commercially available models.
Until then, I had refused direct engagement with such systems, for any purpose whatsoever, but I could not look away any longer, especially due to what I understood about its impending impact on the journal business.
We set out to share our experiences, exchange technical tips, discuss the latest news, and try to understand this better. Rather quickly, the seminar evolved into more of a "support group", where we would joke at the latest over-stretched analogy, speculate on optimistic/pessimistic futures, admit to our token dependencies, and express our grief.
The working group has reached a natural coda, as the department (with broader university backing) has just set up a broader committee to grapple with the big shifts underway.
I learned a lot through the working group, went through a lot of phases, and am grateful to the other members for walking together in this journey. Building and strengthening connections, sharing and reflection with others, this is how we move forward in this.
#generativeAI #formalization #semiautomatic #lean #scientificpublishing
-
Just dropped two new papers into the arxiv:
https://arxiv.org/abs/2607.12461
http://arxiv.org/abs/2607.17421
This caps off an extraordinary arc, the true seed of which was harshly interrupted by Covid, curling over multiple personal life changes, ending during a dawn in the dominance of AI-augmented mathematics.
Aside from the significant progress on one of my personal favourites ---indeed a *classic* Erdos problem--- what might be of wider interest is our use of (semiautomatically generated) Lean to corroborate the fidelity of computationally-aided proof methods (in this case, a nontrivial variant of flag algebras).
Oh, and let me extend my congratulations to all the Eoins.
#eoins #combinatorics #generativeAI #formalization #semiautomatic #lean #covid
