Syzygies

I just ended my Cursor subscription today, and upgraded from Claude's Pro to Max plan to reduce my Claude Code costs. They now include a healthy Claude Code allowance in the Max plans.

If one has already set up Claude Code with metered API use, one toggles between plans using the /login command. Once to start using Max, then whenever one hits a five hour rate limit and wants to keep working.

I've tried many platforms. I kept Cursor long after Windsurf, but Claude Code is a clear winner, as most people report who don't bristle at the cost.

When Cursor or Windsurf forks VS Code, they have a reason. Their chat panes always felt like periscopes; one has better control over Claude Code in a terminal, and this frees up one's choice of editor. I now use Sublime Text, fast and lean.

Yes!

I used to divide my time between a concrete hulk of a NYC apartment building, and a California home insulated to notoriously poor California standards. I was plenty warm in New York winters just from my neighbors' heat nearly all of the time. In California, there was a narrow window (think "Apollo 13 re-entry") between too cold and too warm.

Then we modernized ceiling fans, and I hit on running them in "winter mode" drawing hot air up to flow back down the walls. Bingo! I love that ISO 7730 confirms this.

"I bought those expensive knives. Why doesn't my cooking taste better?"

"I picked up an extraordinary violin once. It sounded awful!"

There's an art here. Managerial genius is recognizing everyone's strengths and weaknesses, and maximizing impact. Coding with AI is no different.

Of course I have to understand the code well enough to have written it. Usually much of the time is spent proposing improvements.

I'm a few months in, learning to code with AI for my math research. After a career as a professor, I'm not sure I could explain to anyone what I'm starting to get right, but I'm working several times more efficiently than I ever could by hand.

Some people will get the hang of this faster than others, and it's bull to think this can be taught.

When my father bought his first digital camera, he insisted on raw format access.

Inexplicably I didn't understand at the time why he (Bryce Bayer) wanted this. He was modest about his work.

I do now!

That's what I learned from!

Cloudless Fluid requires a Teams Enterprise subscription. Or one can manually enter IP addresses. Their default is cloud mediation, so yes, they presume a working internet connection.

Their UKH 80 looks incredible.

Software is as critical as hardware: The UHK supports holding a key down to select a different keymap layer, then using the other hand to tap a key in that layer. While few people learn many-key chording, "one finger each hand" is every bit as easy as ordinary typing, with practice. This supports an n^2 expansion in effective keyboard reach. I'm surprised this isn't the norm for selecting Chinese/Japanese characters.

The question is: How well? I'm not entirely happy with my QMK firmware implementation. Tap-hold is the antithesis of n-key rollover; one needs to learn to properly nest key-down, key-up events. It's easy to switch from a clarinet (cleanly cover holes) to a saxophone (slap pads), but hard switching back. And we've all learned to type like we're on a saxophone, relying on n-key rollover to cover many sins.

I now use QMK firmware with Hasu controllers for multiple Leopold FC660C keyboards with Topre Silent 45g "rubber dome" key switches. After trying dozens of mechanical key switches, I found that nothing feels like a Topre switch.

And here's the kicker: The physical form factor doesn't matter so much if your fingers rarely go far from home row, which is what tap/hold facilitates.

I've been saving Markdown transcripts of my more involved AI chats, and I was unhappy with how any tool rendered to PDF. In either Cursor or Windsurf, I had Claude 3.5 Sonnet code a Ruby script for me that converts Markdown to Typst, a LaTeX alternative that looks a lot like Markdown. Typst offers beautiful formatting control for the output PDFs.

Mathematicians see hundreds of delusional papers over a career. It takes seconds to read their "no one understands me, I'm trying to save the world" tells. Every seen a Dr. Bronners soap label? Yep, that guy was crazy too.

We're also good at spotting novel ideas, and making odds on potential failure points. A good paper telegraphs their approach.

Post on a legitimate archive server, and wait. You'll get read. If nothing else, you'll make the next AI training corpus.

Do you have a car?

Do you really want to wait for humans to reprogram air traffic control software unassisted, with no formal correctness guarantees?

Your attitude is fine if you plan to walk everywhere.

"For documents whose source is likely to be shared or handed over to other pe ople, writing in TeX rather than expecting them to learn a new language is still good citizenship."

Conversely, my entire interest in Typst is have an input format more efficiently read by AI. We've passed the inflection point where one can responsibly only write for humans.

Typst is Markdown-adjacent, while PreTeXT is XML-adjacent. More characters but even easier for AI to process. I'd switch for the HTML and ePub support, but no syntax coloring for code blocks?

I'm at a math conference where an amazing speaker brought up this list; she was on it.

People eligible for DEI funding are often encouraged to choose that channel over a "regular" channel, in which they might easily have been awarded funding. This inevitable adaptation is what happens when one puts filters on cigarettes, designs tax laws... To cut this funding for existing awardees would be overt discrimination.

"Outreach" language is a requirement for NSF grants. I'm surprised that a majority of the grants overall didn't trigger their search filters. It is likely that they restricted their search to these DEI channels.

Of course Ted Cruz knows this. What I don't know is if he's actually a bigot, or a maggot who knows his supporters are bigots.

Yes. There are better and worse ways to lead a team, just as there are better and worse ways to prompt AI.

This post reads as a description of how the wheels come off the wagon if you don't do things well.

With the evolution of AI agents, we'll all be virtual CTOs whether we like it or not, mastering scale whether we like it or not. We need to learn to do things well.

Managerial genius will be the whole ball of wax.

An environment such as Cursor supports many approaches for working with AI. "Chat" would be the instructions printed on the bottom, perhaps how their developers use it, but far from the only mode it actually supports.

It is helpful to frame this in the historical arc described by Yuval Harari in his recent book "Nexus" on the evolution of information systems. We're at the dawn of history for how to work with AI, and actively visualizing the future has an immediate ROI.

"Chat" is cave man oral tradition. It is like attempting a complex Ruby project through the periscope of an `irb` session. One needs to use an IDE to manage a complex code base. We all know this, but we haven't connected the dots that we need to approach prompt management the same way.

Flip ahead in Harari's book, and he describes rabbis writing texts on how to interpret [texts on how to interpret]* holy scriptures. Like Christopher Nolan's movie "Inception" (his second most relevant work after "Memento"), I've found myself several dreams deep collaborating with AI to develop prompts for [collaborating with AI to develop prompts for]* writing code together. Test the whole setup on multiple fresh AI sessions, as if one is running a business school laboratory on managerial genius, till AI can write correct code in one shot.

Duh? Good managers already understand this, working with teams of people. Technical climbers work cliffs this way. And AI was a blithering idiot until we understood how to simulate recursion in multilayer neural nets.

AI is a Rorschach inkblot test. Talk to it like a kindergartner, and you see the intelligence of a kindergartner. Use your most talented programmer to collaborate with you in preparing precise and complete specifications for your team, and you see a talented team of mature professionals.

We all experience degradation of long AI sessions. This is not inevitable; "life extension" needs to be tackled as a research problem. Just as old people get senile, AI fumbles its own context management over time. Civilization has advanced by developing technologies for passing knowledge forward. We need to engineer similar technologies for providing persistent memory to make each successive AI session smarter than the last. Authoring this knowledge helps each session to survive longer. If we fail to see this, we're condemning ourselves to stay cave men.

Compare the history of computing. There was a lot of philosophy and abstract mathematics about the potential for mechanical computation, but our worldview exploded when we could actually plug the machines in. We're at the same inflection point for theories of mind, semantic compression, structured memory. Indeed, philosophy was an untestable intellectual exercise before; now we can plug it in.

How do I know this? I'm just an old mathematician, in my first month trying to learn AI for one final burst of productivity before my father's dementia arrives. I don't have time to wait for anyone's version of these visions, so I computed them.

In mathematics, the line in the sand between theory and computation keeps moving. Indeed, I helped move it by computerizing my field when I was young. Mathematicians still contribute theory, and the computations help.

A similar line in the sand is moving, between visionary creativity and computation. LLMs are association engines of staggering scope, and what some call "hallucinations" can be harnessed to generalize from all human endeavors to project future best practices. Like how to best work with AI.

I've tested everything I say here, and it works.

I'm trying to sort out whether this article is relevant to a problem I've been working on the last few days. (It's staggering how deploying AI changes time scales.)

We need "Centaur" documentation that can efficiently transfer information formerly targeting humans, to AI. To fit within current token windows, one needs semantic compression. What data representation would be ideal for this?

This seems so obvious once you consider it, it becomes impossible to explain why OpenAI or Anthropic or Cursor or Windsurf don't offer "knowledge packs" that can transfer their documentation to AI. Of course, it's frequently the case that people who make tools don't "get" them.

My immediate need is to condense the Lean 4 website into a Claude 3.5 Sonnet context window. No AI can code in Lean 4 reliably (not that many humans either ;-) but I don't want the Lean / AI choice to be either / or.

My father (Bryce Bayer) was known for the Bayer filter, which survives to this day as the dominant approach to capturing color images in all digital cameras, and Bayer dithering, which didn't. Last time I saw it used was as decoration on DEC computer boxes.

In grad school, I went "down the street" to MIT to hear him speak. I overheard some students disparaging this dithering as primitive. Hey, you try living in the past and seeing the future!

I love HN for its healthy love of history.

I'm running tests for an involved math research project, and to my great surprise Lean 4 << Haskell << OCaml in execution times (so far).

I love Lean 4, but good luck getting help with it from AI. Today's project-in-progress is digesting their reference manual to fit well within a 200K context window. We'll see if that helps.

In this thread you're seeing survivorship bias. We're discussing an editor that doesn't support AI.

AI is Rashomon. It's just an association engine of immense scope. We're not talking to an alien intelligence; we're talking to ourselves. It's an existential mirror, and each person's experience will vary. Some people can control the dance of the campfire flames. Some people just aren't cut out to be shamans.

Evolution is always making failed experiments, as a hedge against catastrophic ecosystem change. I'm convinced that neurodivergents are better suited to becoming AI Centaurs, in the sense Gary Kasparov promoted after he came to terms with his chess loss to IBM's Big Blue.

I made my career by computerizing a branch of mathematics that did not want to cooperate. Now in retirement, I see AI as the key to achieving my dreams before my father's dementia arrives. It has radically transformed my past month.

My preferred language is Lean 4, and AI has as hard a time coding in it as people. This morning's retooling has been distilling the Lean 4 website down to fit well within a 200K token context window. I prefer AI chat at arms length so I make the mistakes not it, but with enough editor integration that we can both see what we're doing.

I loved Sublime Text when I used it. And AI coding doesn't primarily accelerate one's original spec, it encourages tool scopes one might never have dared attempt. So writing a Sublime Text plugin that interfaces with an Anthropic API key is something any of us could probably knock off.

Deepseek r1 is getting a lot of buzz in the last day or so. As a Chat agent in Cursor, it gets further than I've seen other AI get at writing Lean 4 code.

The process is acutely painful. It can't stick to directions, and keeps trying to add proof features that it can't get to work, despite my instructions that we're using Lean 4 as a general purpose programming language.

To my surprise, the code ran faster than either Haskell or Rust on a small case. There could be so many artifacts involved in such a conclusion, but larger cases blew the stack. That's just inexperienced code.

I love Lean 4 as a general purpose programming language, but I can't use it because no current AI coding assistant can reliably work with me in Lean. I can be trying six languages at once like a chess master playing an exhibition simultaneous match, and they'll all flow in Cursor using Claude 3.5 Sonnet, or even Windsurf. Then add Lean 4 and everyone chokes.

On the other hand, Claude 3.5 Sonnet understands my iPad math drawings better than my colleagues. I am admittedly weird, but AI as an association engine of incomprehensible scope likes trippy. Trippy helps its reach. Philosophy never really worked until now when you can run it on a computer. AI really rewards recursive meta; it picks up speed like ice sailing. We're would-be shamans sitting around the fire a million years ago, imagining we can control the dance of the flames. With AI, we can.

Claude also understands, say, computational group theory or strategies for combinatorial enumeration, remarkably well. So it can assist in math research.

Formal proofs in Lean 4 may be hard to read, but the elephant in the room is how hard conventional math papers are to read. We're terrible at expressing ourselves, so reading a paper is the equivalent of reverse-engineering bad computer code to reconstruct thoughts the author failed to express. And it's embarrassing in 2025 that conventional papers can't be automatically checked.

A new genre will emerge in between: In the "Centaur" model Gary Kasparov popularized after he recovered from his chess defeat by IBM's Big Blue, we want papers to actually be very careful, battle-tested prompts for AI. They will pass as conventional papers for mathematicians still trapped in amber, but they're really just prompts for both us and AI.

The documentation for Lean 4 is aimed at humans. If it were designed to be a hybrid "Centaur" prompt doc, perhaps my tools would be better able to help me code in Lean 4.

My mind is blown, a new language where I can see new reach. Back in the day, APL was good at multidimensional arrays, and from there could outstrip Fortran shops at anything. A surprising swath of discrete reality can be viewed as a graph, or graphs of graphs. For me, computational group theory, combinatorial enumeration, canonical forms... All topics Claude 3.5 Sonnet happens to be exceptional at.

Even a month ago, I'd have asked "Where's the parallelism?" looking at any new language. AI has upended my world. My subscriptions are getting out of hand, they're starting to look like some peoples' sports channel cable bills. I'll be experimenting with the right specification prompt to get AI to write correct programs in three languages side by side, in either Cursor or Windsurf. Then ask it to write a better prompt, and go test that in the other editor. I'm not sleeping much, it's like buying my first Mac.

One constant debate I have with Claude is how much the choice of language affects AI reasoning ability. There's training corpus, but AI is even more appreciative of high level reasoning constructs than we are. AI doesn't need our idioms; when it taught itself the game Go it came up with its own.

So human documentation is nice, but who programs that way anymore? Where's the specification prompt that suffices for Claude to code whatever we want in Dusa?

Exactly. These tools test whether we're brilliant managers, understanding the potential and limitations of everyone we manage, and understanding the work well enough to do it ourselves.

I too am using AI to play with new languages and problem domains, and to write tools I've long wanted but never found time to implement. I find it helpful to ask other LLMs about best practices, with no conflict of interest where they're trying to write me code.

For my initial experiences with Windsurf Editor, the AI got ahead of me and then into trouble it couldn't resolve, thrashing in ways my daughter learned to avoid in her first semester of programming. I've found Claude 3.5 Sonnet understands the problems I work on best, so I'll use Cursor for access to this AI. Workflow enhancements are secondary to the underlying intelligence.

I've stopped expressions of outrage at lazy first answers, after seeing some sort of "code of conduct" warning.

Apparently, the singularity ship has sailed, but we really don't want AI to remember us as the species that cursed abuse at it when it was a puppy.

Our world is increasingly defined by software without correctness proofs. Our tools are too clumsy, and we're just not smart enough, so we accept this situation. AI-verified code could become one of the most economically important applications of machine learning, when we cross the threshold where this becomes feasible.

I'm a mathematician, and we struggle with the purpose of a proof: Is it to verify, or also to explain so we can generalize? Machine proofs tend to be inscrutable.

While "the singularity" is unlikely anytime soon, we should recall that before the first atomic test there were calculations to insure that we didn't ignite the atmosphere. We're going to need proofs that we have control of AI, and there's an obvious conflict of interest in trusting AI's say so here. We need to understand these proofs.

Wow! My first test query immediately found me a paper relevant to research code I'm writing. Down that rabbit hole, I almost forgot to come back and praise this project.

"Can AI do math for us" is the canonical wrong question. People want self-driving cars so they can drink and watch TV. We should crave tools that enhance our abilities, as tools have done since prehistoric times.

I'm a research mathematician. In the 1980's I'd ask everyone I knew a question, and flip through the hard bound library volumes of Mathematical Reviews, hoping to recognize something. If I was lucky, I'd get a hit in three weeks.

Internet search has shortened this turnaround. One instead needs to guess what someone else might call an idea. "Broken circuits?" Score! Still, time consuming.

I went all in on ChatGPT after hearing that Terry Tao had learned the Lean 4 proof assistant in a matter of weeks, relying heavily on AI advice. It's clumsy, but a very fast way to get suggestions.

Now, one can hold involved conversations with ChatGPT or Claude, exploring mathematical ideas. AI is often wrong, never knows when it's wrong, but people are like this too. Read how the insurance incidents for self-driving taxis are well below the human incident rates? Talking to fellow mathematicians can be frustrating, and so is talking with AI, but AI conversations go faster and can take place in the middle of the night.

I don't want AI to prove theorems for me, those theorems will be as boring as most of the dreck published by humans. I want AI to inspire bursts of creativity in humans.

For anyone who ran out of patience scrolling, and prefers their information top-down: https://en.wikipedia.org/wiki/1955_Le_Mans_disaster

I too kept a log of my errors in the 1980's, hoping to become a better C programmer. I imagined that with careful enough reflection, I would never make the same mistake twice.

I found the log many years later. Last entry: "Forgot to eat. Got sick."

This article is missing the "meta" in studying mathematics.

Creative introspection into how one learns begins to really pay off partway through college.

One's relationship to convention becomes as important as one's relationship to technique. Understanding the "whole" of something involves understanding the biases that shape the presentation you're seeing. You'll probably want to shed them.

This applies whether one wants to change math or just learn it. A passive stance, trying to do what others want, is a recipe for frustration.

I grew up with no choice in this matter. Then there was a period when "touch" dialing was available for an exhorbitant premium.

There's something so Brooklyn / Portland about wanting to relive this for the romance. It sucked.