Syzygies

I was hoping for Lean 4.

J is unclear on the concept, it's a hack to port APL to ASCII. I'm typing on a ZMK keyboard now where an APL unicode layer would be trivial. There are modern APLs. One can code a iOS keyboard with AI help.

While a native APL would be nice, the cloud solution would be robust access to a professional product. Build the chain via existing tools to bridge the iPad to APL running on a desktop machine.

I looked into this recently; but I've decided on Lean 4 as the successor "best language in existence" for my needs.

My recent language comparison: https://github.com/Syzygies/Compare

My APL one-liner story: https://news.ycombinator.com/item?id=27460887

Julia is reasonably fast. I returned to a language comparison project specific to my math research, to see how I might do better. My agents and I studied the advice in the post and various more recent links from the comments, but we were already mostly on target and nothing left moved the needle.

My work is more combinatorial. Julia does excel at numerical computation. There's a tribal divide in math between people who can't go 30 seconds away from the real or complex numbers, and those whose tolerance is about that long. I try to keep an open mind, but I'm closer to the second camp. Julia is good enough to consider either way.

A development in recent months, AI can assist in general purpose Lean 4 programming, no longer getting confused by the dominant proof-oriented training corpus. If one is a functional programmer who believes that Haskell was on the right track, then Lean is the most interesting language choice for shaping one's thoughts. Benchmarks are inherently misleading if a better language makes it possible to express algorithms out of reach of more primitive languages.

https://github.com/Syzygies/Compare

            C++  100    13.08s  ±0.08s
           Rust   99    13.16s  ±0.02s
          Julia   90    14.54s  ±0.01s
             F#   90    14.54s  ±0.04s
  Kotlin-native   88    14.79s  ±0.01s
         Kotlin   86    15.18s  ±0.01s
          Scala   79    16.50s  ±0.08s
   Scala-native   76    17.14s  ±0.02s
            Nim   65    20.17s  ±0.01s
          Swift   64    20.54s  ±0.04s
          Ocaml   52    25.38s  ±0.04s
           Chez   49    26.64s  ±0.02s
        Haskell   37    34.96s  ±0.06s
           Lean   29    45.39s  ±0.15s

I have thousands of dollars of mechanical keyboards I could sell on eBay, if only I wanted to take the time to remember how I last left the firmware reset sequence.

I set them all aside for several Leopold FC660C Topre keyboards with the Hasu mod supporting QMK firmware.

Then I started getting ulnar nerve issues, either the gym or too many AI prompts. I discovered MoErgo's keyboards, and their custom Cherry Blossom switches. I honestly believe they have subtle design genius pervading their work, beyond anything I have ever experienced. Quiz me; I've also tried X.

Their Glove80 could use a bit of the "door slams like a Rolls-Royce" quality that many of these bespoke keyboard makers apply to more conventional designs. The design nevertheless triumphs.

Their second generation Go60 is my "Stay60" I can't give up. The build quality, and I don't want more keys.

At first it feels like the Cherry Blossom switches fire from a breeze with the window open. One adapts.

Yes, that project. I keep thinking I'm done, but it's so much fun being a language tourist.

I admire Clojure, and Rich Hickey's deep experience and knowledge of languages that he brought to the table. Clojure bottomed out for my comparison.

Perhaps an expert could strike a better balance, but it struck me and my various agents that we'd be fighting the language to make it faster.

https://github.com/Syzygies/Compare

Any benchmarks? I have a combinatorial enumeration comparison project where the .NET jit optimized my hot loops for F# to in some cases matching Rust performance. F# is inspired by OCaml, and for me F# runs twice as fast.

Scala got a face lift where indentation replaces syntax, a modern poetry look many of us can't live without. It is entirely practical to eliminate most parentheses from Lisp (I have written thousands of lines of Scheme this way, hands down my favorite code to read), but doing so will lead to a tribal swarm attack. It is also easy to train Common Lisp to lay off the caps, but any stock installation greets users with an old man shouting (GET OFF (MY LAWN)).

The idea of Lisp is pure genius. One wonders where we would be today if any Lisp took a more pragmatic attitude towards encouraging adoption.

LLM's are an extension of us. We sometimes have to work to learn something new; so do LLM's. It's all in how we manage that process. Reifying information is the whole ball of wax, what separates different people's success rates using AI. AI is more surfboard than self-driving car; you don't just tell it which way to go.

I still can't get AI to code well in Lean 4, but I'm writing a parser for a language that doesn't exist. AI understands the language as well as I do.

Yes, Chez improved a bit, at the expensive of readability.

The common theme is diverse notions of a language. When I order from a menu, I don't order based on price, but I prefer to see the prices.

Lean 4 is the most interesting language on my list. I didn't reject it on price.

Thank you. I will try your Chez idea. I love Chez, even if coding in Scheme can feel like rubbing sticks together to start a fire on an island, when e.g. Scala has induction ranges. And I didn't try Idris or Racket as they compile to Chez, but perhaps they do so better than I did.

As for parallelism this is a primary concern of mine, and I tried multiple approaches for every language where there was a choice. I used my own work-stealing code only when it beat standard libraries. AI warned me I was in over my head, that writing such a library takes years of experience, but my use case (and my expected use cases in my research) is so uniform that simple can win, minimally touching the required bases such as permuting tasks to avoid false sharing.

I don't believe that the JIT languages (F# on top) do so well because of better parallelism. This is branch optimization. For this use case an AOT compiler with ample benchmark data to influence output should do better. That isn't a thing, and the argument seems to be that few use cases stay consistent. A JIT can adapt.

I recently revisited a language comparison project, a specific benchmark tallying the cycle decompositions in parallel of the 3,715,891,200 signed permutations on 10 letters. I kept a dozen languages as finalists, different philosophies but all choices I could imagine making for my research programming. Rather than "ur" I was looking for best modern realizations of various paradigms. And while I measured performance I also considered ease of AI help, and my willingness to review and think in the code. I worked hard to optimize each language, a form of tourism made possible by AI.

The results surprised me:

             F#  100    19.17s  ±0.04s
            C++   96    19.92s  ±0.13s
           Rust   95    20.20s  ±0.38s
         Kotlin   89    21.51s  ±0.04s
          Scala   88    21.68s  ±0.04s
  Kotlin-native   81    23.69s  ±0.11s
   Scala-native   77    24.72s  ±0.03s
            Nim   69    27.92s  ±0.04s
          Julia   63    30.54s  ±0.08s
          Swift   52    36.86s  ±0.03s
          Ocaml   47    41.10s  ±0.10s
        Haskell   40    47.94s  ±0.06s
           Chez   39    49.46s  ±0.04s
           Lean   10   198.63s  ±1.02s

https://github.com/Syzygies/Compare

I'm a retired mathematician hoping to finish a second proof of a major theorem before I die. AI needs to understand my math and help me code. What I spend on AI isn't going to deplete my retirement savings.

So far, Opus 4.7 seems a bit smarter than Opus 4.6 for my use case. That's my only concern. Is an $80 bottle of wine a better value than a $20 or $40 bottle of wine? Pretty much never. If there are those of us willing to buy $80 bottles of wine, of course the market will facilitate this.

People can use whatever model they want. I'm too worried about worms crawling through my dead body to waste time on any but the smartest model any moment can offer.

There are many duality theories in mathematics where both of these perspectives are valid. Each instance is "Duh! What's going on here is just..." and the pragmatic move nimbly through each instance without concern. For others, the potential theory IS the object of interest. Is this apparent pattern a deep principle or just a mirage? When something is actually going on, one learns powerful new techniques by recognizing a precise pattern.

I've stumbled onto deeply disguised dualities in my career. (One could argue with a straight face there are only two, but this is not formalized.) It's more a psychological process than a technical one.

It's always possible to ignore that one is standing in a tree farm. Trees have such interesting bark.

It comes down to are you reading to write, or reading to think?

Zettelkasten facilitates publication dysentery, which is already out of hand. I have the same problem with conventional bibliography managers. I have a few thousand papers and books on my computer, woven with the beginnings of a mind-mapping system. I recoil every time I consider using software "designed" for this, which excels at cranking out papers but not at deftly flying through idea space. And idea space is an actual thing now, that "King - Man + Woman = Queen" linear algebra supporting AI. Ignore this and one is selling buggy whips.

Reifying memory is the next frontier for LLMs, with many efforts underway. That should be our defining use case for mind-mapping.

Hearing my "before I die" math and code ambitions, a psychiatrist friend tried to convince me to hire a full-time programming assistant. Then came AI.

Money is relative. I retired at less than the average professor salary (all ages) at a not-rich school. I would have made more in tech. I still have weeks where the market goes up 2000x my AI budget, just the retirement savings from my salary. Anyone who isn't living in a van and eating peanut butter if they must, to save the max toward retirement, isn't recognizing how profoundly our system is rigged to favor saving.

That's funny. My paper on digital timestamping is one of eight references in the original bitcoin paper. You'd think if anyone was serious about unmasking her they would have asked me.

>The way I use Claude is quite similar to what super powers does under the hood anyways.

I bake my own bread and solo code, both episodic. No matter how I vary fresh starts, I always end up in the same place. The optimization problem feels to be a giant bowl.

This reminds me of named flavors of management style for teams of programmers. A friend in this role instead prefers deep dives into Apollo flight control, and abstracting.

As a solo programmer I always converge on staying extraordinarily involved in planning and code review, and working in steps of finer granularity than superpowers suggests. One may produce less code this way, but it's the only way I know to discover one needs less code.

Yes, "fucking" stood out for me, too. The rest of the text very much has the feel of AI writing.

AI agents routinely make me want to swear at them. If I do, they then pivot to foul language themselves, as if they're emulating a hip "tech bro" casual banter. But when I swear, I catch myself that I'm losing perspective surfing this well-informed association echo chamber. Time to go to the gym or something...

That all makes me wonder about the human role here: Who actually decided to create a blog post? I see "fucking" as a trace of human intervention.

I began studying 3-manifolds after coming up with a novel way I preferred to draw their presentations. All approaches are formally equivalent, but they impose different cognitive loads in practice. My approach was trivially equivalent to triangulations, or spines, or Heegaard splittings, or ... but I found myself far more nimbly able to "see" 3-manifolds my way.

I showed various colleagues. Each one would ask me to demonstrate the equivalence to their preferred presentation, then assure me "nothing to see here, move along!" that I should instead stick to their convention.

Then I met with Bill Thurston, the most influential topologist of our lifetimes. He had me quickly describe the equivalence between my form and every other known form, effectively adding my node to a complete graph of equivalences he had in his muscle memory. He then suggested some generalizations, and proposed that circle packings would prove to be important to me.

Some mathematicians are smart enough to see no distinction between any of the ways to describe the essential structure of a mathematical object. They see the object.

We're in agreement. I understand how much harder it is to "think with AI"; the last year of my life has been a brutal struggle to figure this out.

I also agree that neural net LLMs are not the inevitable way to implement AI. I'm most intrigued by the theoretical underpinnings of mathematical proof assistants such as Lean 4. Computer scientists understand the word problem for strings as undecidable. The word problem for typed trees with an intrinsic notion of induction is harder, but constructing proofs is finding paths in this tree space. Just as mechanical computers failed in base ten while at the same time Boole had already developed base two logic, I see these efforts merging. Neural nets struggle to simulate recursion; for proof assistants recursion is baked in. Stare at these tree paths and one sees thought at the atomic level, begging to be incorporated into AI. For now the river runs the other way, using AI to find proofs. That river will reverse flow.

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI.

A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go.

Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of life because we're a selfish species. In contrast Niki Lauda trusted fellow Formula 1 race car driver James Hunt to race centimeters apart. Some people want AI to help them drive that well. They'll have great jobs as AI evolves.

Gary Kasparov pioneered "freestyle" chess tournaments after his defeat by Big Blue, where the best human players were paired with computers, coining the "centaur" model of human-machine cooperation. This is frequently cited in the finance literature, where it is recognized that AI-guided human judgement can out-perform either humans or machines.

Any math professor knows how to help graduate students confidently complete a PhD thesis, or how to humiliate students in an oral exam. It’s a choice. To accomplish more work than one can complete alone, choose the former. This is the arc of human evolution: we develop tools to enhance our abilities. We meld with an abacus or a slide rule, and it makes us smarter. We learn to anticipate computations, like we’re playing a musical instrument in our heads. Or we pull out a calculator that makes us dumber. The role we see for our tools matters.

Programmers who actually write better code using AI know this. These HN threads are filled with despair over the poor quality of vibe coding. At the same time, Anthropic is successfully coding Claude using Claude.

> Isn't a waste to essentially reinterpret an entire program that may be run 5000 times a day?

This is a dated prejudice that I shared.

To get started coding with AI I made a dozen language comparison project for a toy math problem. F# floored me with how fast it was, nearly edging out C and Rust on my leaderboard, twice as fast as OCaml, and faster than various compiled languages.

Compiling could in principle be fastest, if we had compilers that profiled hours of execution before optimizing code, and only then for "stable" problems. No one writes a compiler like this. In practice, Just In Time interpreters are getting all the love, and it shows. They adapt to the computation. My dated prejudice did not allow for this.

He probably uses Phillips head screws.

(4A = Fourth Amendment, "unreasonable searches and seizures")

Back in 2001 I was the math consultant for "A Beautiful Mind". One spends a lot of time waiting on a film set. Eventually one wonders why.

The majority of wait time was the cinematographer lighting each scene. I imagined a workflow where secondary digital cameras captured 3D information, and all lighting took place in post production. Film productions hemorrhage money by the second; this would be a massive cost saving.

I described this idea to a venture capitalist friend, who concluded one already needed to be a player to pull this off. I mentioned this to an acquaintance at Pixar (a logical player) and they went silent.

Still, we don't shoot movies this way. Not there yet...

Yes. I've been using it today with Zed (a mind-blowing editor, by the way).

One must use an API key to work through Zed, but my Max subscription can be used with Claude Code as an external agent via Zed ACP. And there's some integration; it's a better experience than Claude Code in a terminal next to file viewing in an editor.

One of my side projects has been to recover a K&R C computer algebra system from the 1980's, port to modern 64-bit C. I'd have eight tabs at a time assigned files from a task server, to make passes at 60 or so files. This nearly worked; I'm paused till I can have an agent with a context window that can look at all the code at once. Or I'll attempt a fresh translation based on what I learned.

With a $200 monthly Max subscription, I would regularly stall after completing significant work, but this workflow was feasible. I tried my API key for an hour once; it taught me to laugh at the $200 as quite a deal.

I agree that Opus 4.5 is the only reasonable use of my time. We wouldn't hire some guy off the fryer line to be our CTO; coding needs best effort.

Nevertheless, I thought my setup was involved, but if Boris considers his to be vanilla ice cream then I'm drinking skim milk.

Mathematicians get enamored with particular ways of looking at things, and fall into believing this is gospel. I should know: I am one, and I fight this tendency at every turn.

On one hand, "rational" and "algebraic" are far more pervasive concepts than mathematicians are ever taught to believe. The key here is formal power series in non-commuting variables, as pioneered by Marcel-Paul Schützenberger. "Rational" corresponds to finite state machines, and "Algebraic" corresponds to pushdown automata, the context-free grammars that describe most programming languages.

On the other hand, "Concrete Mathematics" by Donald Knuth, Oren Patashnik, and Ronald Graham (I never met Oren) popularizes another way to organize numbers: The "endpoints" of positive reals are 0/1 and 1/0. Subdivide this interval (any such interval) by taking the center of a/b and c/d as (a+c)/(b+d). Here, the first center is 1/1 = 1. Iterate. Given any number, its coordinates in this system is the sequence of L, R symbols to locate it in successive subdivisions.

Any computer scientist should be chomping at the bit here: What is the complexity of the L, R sequence that locates a given number?

From this perspective, the natural number "e" is one of the simpler numbers known, not lost in the unwashed multitude of "transcendental" numbers.

Most mathematicians don't know this. The idea generalizes to barycentric subdivision in any dimension, but the real line is already interesting.