Comments

• ZettelDistraction

  October 2 edited October 2

  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.

  Zettel GitHub. Zettel Wiki Erdős #2. Problems worthy of attack prove their worth by hitting back. -- Piet Hein. PROBLEMS. Grooks, 1966. CC BY-SA 4.0.
• ctietze

  October 2

  @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

  Author at Zettelkasten.de • https://christiantietze.de/
• ZettelDistraction

  October 2

  @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.

  Zettel GitHub. Zettel Wiki Erdős #2. Problems worthy of attack prove their worth by hitting back. -- Piet Hein. PROBLEMS. Grooks, 1966. CC BY-SA 4.0.
• ZettelDistraction

  October 2

  Lies within a range defined by Fin.

  Zettel GitHub. Zettel Wiki Erdős #2. Problems worthy of attack prove their worth by hitting back. -- Piet Hein. PROBLEMS. Grooks, 1966. CC BY-SA 4.0.