What's happening in your ZK this month, October 2026?

Will_Jenkins

The idea: a general chat about what we're working on currently.

---

Evermore increasing expectations at work leave me with limited time, but especially limited energy, to work on my Zettelkasten. But ironically, I am using what time and energy I have to work on finding a new job. So right now my notes are all about interviewing skills.

Using the tags and flowing inline links I talked about in my previous post, I have a nice structure note now:

I miss the days when I could choose my topics for note taking with more freedom, but I have to get my priorities straight. Having said that, I know it's not healthy to only have a job search to focus on outside of work, so I'm setting aside some time for relaxation and fun too.

"You're allowed to be human" ... one of the best things I've ever read. It was in a psychology book, but I think it's good to hear or read it from any source. I do believe it's something we should remind ourselves of: We're allowed to be human.

---

And how is it going for the rest of you? What's happening in your Zettelkasten this month?

ZettelDistraction

In my backwards way of doing things, I use my Zettelkasten as a lab notebook to track my progress with various projects, such as Pointwise provable equality and the failure of composition.

The story is that one of two constructions described in papers I was relying on for another project was fatally flawed. (It made assumptions violating Gödel's second incompleteness theorem; there is another proof avoiding the second incompleteness theorem.) The construction appeared in two refereed papers, the first published in the Notre Dame Journal of Formal Logic, and the second in The Journal of Symbolic Logic. Because the papers had undergone peer review, I decided to formalize the proof of the flawed construction in the Lean proof assistant and register the formalization in the Palomar Registry.

That detour was good news, since it eliminated one half of the examples I needed to formalize for the original project I was and still am working on.

ctietze

@Will_Jenkins Thanks for keeping this up in October! 💪

*  *  *  *  *  *  *  *  *  

@ZettelDistraction I clicked around and didn't understand anything, but the .lean file looked really clean. What a language

Since I'm a noob, I can only ask newbie questions: why did you pick the form

def fin0 {n : ℕ} : Fin (n + 1) := ⟨0, Nat.zero_lt_succ n⟩
def fin1 {n : ℕ} : Fin (n + 2) := (fin0 (n := n)).succ
def fin2 {n : ℕ} : Fin (n + 3) := (fin1 (n := n)).succ
def fin3 {n : ℕ} : Fin (n + 4) := (fin2 (n := n)).succ

where a fin0 and a recursive generalization for finN would've been possible? I asked the tutor bots of course whether Lean supports these kinds of statements as a proof assistant (Agda does!) but it sounded like bit of a hassle, even though perfectly possible to write. The ℕ type probably does something like that under the hood and 4 names aren't exactly too much to bear or maintain. Just curious about your proof assistant reasoning there!

*  *  *  *  *  *  *  *  *  

Last month I upgraded some libraries I wrote for apps, including The Archive, to help with new system features and Swift 6.x programming language additions.

I experimented with a Lisp-1 language embedding, Janet, and it's a really nice language to write.
https://learnxinyminutes.com/janet Short intro
https://janet.guide/xenofunctions/ Longer intro

Culminated in the generation of a Swift package, swift-janet, to have a portable way to ship Janet scripts in apps and executables:
https://github.com/CleanCocoa/swift-janet

For that topic I learned about the term "quasiquote", which also applies to Emacs Lisp, but as a concept didn't enter my Zettelkasten before.

*  *  *  *  *  *  *  *  *  

The 'house' department of my Zettelkasten grows slowly as the influx of new information and changes outpaces my capability to carefully create notes. -- Things move too fast for me to catch up! Talking about the same topics over and over is less of an investment, and opposed to Zettelkasten work can be done in a car or at the building site or anywhere, really. So I'm learning more things with my first brain, the old-fashioned way, than with my extended ZK brain

ZettelDistraction

@ctietze said:
@ZettelDistraction I clicked around and didn't understand anything, but the .lean file looked really clean. What a language

Since I'm a noob, I can only ask newbie questions: why did you pick the form

def fin0 {n : ℕ} : Fin (n + 1) := ⟨0, Nat.zero_lt_succ n⟩
def fin1 {n : ℕ} : Fin (n + 2) := (fin0 (n := n)).succ
def fin2 {n : ℕ} : Fin (n + 3) := (fin1 (n := n)).succ
def fin3 {n : ℕ} : Fin (n + 4) := (fin2 (n := n)).succ

where a fin0 and a recursive generalization for finN would've been possible?

It could have been

def finN {n : ℕ} : (k : ℕ) → Fin (n + k + 1)
  | 0 => fin0 (n := n)
  | k + 1 => (finN (n := n) k).succ

Then the names could have been abbreviations

abbrev fin1 {n : ℕ} : Fin (n + 2) := finN (n := n) 1
abbrev fin2 {n : ℕ} : Fin (n + 3) := finN (n := n) 2
abbrev fin3 {n : ℕ} : Fin (n + 4) := finN (n := n) 3

These return a pair consisting of an index, either 0, 1, 2, 3 together with a proof that the index lies within an index.

I don't know why not use recursion. There's no performance penalty.

ZettelDistraction

Lies within a range defined by Fin.

Will_Jenkins

@ZettelDistraction I would love to be able to handle maths at that level, but I'm happy I even remember my school maths at this point. I've taken a Udemy course in maths as a refresher, and intend to get back into both maths and statistics in preparation for a future PhD or DBA (doctor of business administration). I'm not entirely sure what level of maths and statistics ability I would need, but at the very least I'll have to be able to handle some analysis and plotting.

I've considered Operations Research as a possible future career, and knowing what that entails gives me good guidance for what skills I need to develop.

I've never heard of the Lean language before. I'm always amazed how many languages there are out there. That goes for Janet too @ctietze, that's another Lisp dialect I've never heard of. There are so many languages and not enough time to learn them all! I'll be happy to be good at 2 or 3 in the long-run.

Edmund

What are the words of the year? For 2025, I found these: Slop (Merriam-Webster), Rage bait (Oxford English Dictionary), Parasocial (Cambridge Dictionary) and Vibe coding (Collins English Dictionary). All of these words are related to AI. But what are the words of the year from my own Zettelkasten?

I filtered the index of my Zettelkasten by date. I rated the terms for each month, and then rated the resulting shortlist to get the Word of the Year.

Here are my results for 2026: augmented intelligence, clarity, concept map, context principle, family resemblance, generative learning, journey map, mimetic desire, modular thinking, resonance, self directed learning, syntopical reading, technocapitalism, and zone of proximal development. One of them will win the race.

Do you have a word of the year? What criteria did you use to decide?

Will_Jenkins

@Edmund said:
What are the words of the year?

Here are my results for 2026: augmented intelligence, clarity, concept map, context principle, family resemblance, generative learning, journey map, mimetic desire, modular thinking, resonance, self directed learning, syntopical reading, technocapitalism, and zone of proximal development. One of them will win the race.

Do you have a word of the year? What criteria did you use to decide?

My Zettelkasten word of the year is 'friction', as I've changed the way I organize my ZK to reduce friction in it, partly thanks to your book on ZK minimalism, and partly thanks to the blog post The Friction Fallacy.

I realized I was making things too complicated, with too many unnecessary notes, and that it was over-organized. I've simplified things a lot this year, and my ZK has a lot less friction because of it.

Funnily enough, simplifying the organization has made it more organized now, as I can more easily find what I'm looking for, and I enjoy using it more too.