Syzygies

I loved the appearance of Bill Thurston. He proved enough of what he saw to be considered one of our greatest mathematicians, but his brilliance was what he saw.

The obvious question Terry Tao seems not to address: AI mops up our unsolved problems? Whose unsolved problems? The architecture of mathematics will remain a human endeavor long after we replace human construction workers with machines.

Syzygies

Hôm kiadiscuss

The sum from 1 to n is easy various ways, a matter of personal preference. One can "make rainbows", pairing 1 with n, 2 with n-1, ending up with n/2 copies of n+1. I prefer to tear an n by n+1 rectangle of squares in half down its diagonal, to create two copies of 1 + 2 + ... + n.

Gauss famously summed the integers to 100 in school as a kid. It's a litmus test for mathematicians, ask them how they think he did it.

The sum of cubes 1 + 8 + 27 + ... + n^3 happens to be the square of this formula, making it easy from here. Arrange cubes in 4-dimensional space filling out a shape which is the product of two copies of the above triangle of squares illustrating 1 + 2 + ... + n. In other words, working in wxyz space, the shadow in both the wx and yz planes is this triangle. Now rearrange these cubes to form a pyramid with an n by n by n base directly illustrating 1 + 8 + 27 + ... + n^3.

Mathematics is an extraordinary technical accomplishment allowing people to instrument-fly airplanes with the windows painted over. Some of us, most famously Bill Thurston, prefer to look out the window. This exercise is a great example for "feeling" mathematics rather than working around a failure of cognition using formulas.

AI is putting mathematics into crisis. Soon we'll all have AI technical superpowers, and the only meaningful way any of us can excel is by having actual creative vision.

Syzygies

13 ngày trướcdiscuss

> Rich Hickey has a joke about semi-colons in language design

I didn't see semicolons, but I saw plenty of {} braces, and I can't explain why they're needed.

https://github.com/Syzygies/Compare

"I'm already quite sure how I will die: I'll read another article on Hacker News about a new programming language where I see nothing new, and I'll read that they included {}; to make C programmers comfortable. I'll have a massive stroke."

Syzygies

23 ngày trướcdiscuss

> I think most of the substantive criticism of Zuckerberg has been about burning funds.

The 2017 Rohingya massacre in Myanmar? They handed him the death toll. He filed it under growth.

Syzygies

tháng trướcdiscuss

I can't believe I'm the first to Rick roll this thread with the most famous XKCD comic of all time:

https://xkcd.com/327/

Syzygies

tháng trướcdiscuss

I've spoken before a thousand several times saying with a straight face "Every audience is an audience of one."

My first example, I was asked to give one more talk on how one needs to shuffle seven times. There were four people, and a blackboard smaller than my kitchen window. I went for it like I was in office hours, which I've always enjoyed more than teaching. A few weeks later a phone call "I liked your talk." "Thank you." "Could you come to Switzerland to give it again? We can only offer a week's full expenses..."

Then I was asked to write a review of the off-broadway play "Proof" for the American Mathematical Society Notices. I didn't read it much, but I was told people do. I worked a very hard week on my review; my Swarthmore College classmate Ben Brantley's Broadway reviews were life or death for productions at the time, and I didn't want to embarrass myself. Ron Howard read my review, went to see "Proof" twice and loved it, and hired me to be the math consultant for "A Beautiful Mind". That was a transformative experience.

Every audience is indeed an audience of one.

https://www.ams.org/notices/200009/rev-bayer.pdf

Syzygies

tháng trướcdiscuss

I came close to adopting Scala, many parallels to Ruby with vastly better performance.

I'm Ruby or Lean 4.

Syzygies

tháng trướcdiscuss

I nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English.

Lean is designed to be optionally verified; proof is its primary (but not only) application. It seems an impedance mismatch for Jane Street to explore this direction without also migrating to Lean 4.

Syzygies

2 tháng trướcdiscuss

As a mathematician, this reads to me as the most informed comment.

Various priors inoculate me from feeling some of the rejection expressed in other comments. I knew Sammy Eilenberg, perhaps the most famous mathematician to work at Columbia University. He hired me. With friends, I ran into him one night out in NYC, and in his 70's we all stayed out past dawn. His late career focused on topos theory, and everyone in the building politely rolled their eyes. Those are working mathematicians having an understandable reaction; most reactions to topos theory here are simply uninformed. The evolution of programming languages has lead from the lambda calculus to many forms of category theory. Topos theory would not be a surprise.

The Leech lattice? Could be a brilliant idea. Compare Lenstra's elliptic curve factorization algorithm. Sometimes famous landmarks in mathematics have remarkable properties; mining them for algorithmic advantage is no different than mining asteroids for rare metals.

The involvement of AI is most problematic. Mathematics fears being swamped by mediocre AI-authored papers, but the truth is "publish or perish" has long lead to mathematics being swamped by mediocre papers. Bad artists are losing jobs, but good artists are working faster.

I welcome a new era of programming language design, where AI makes rapid prototyping a reality. We just have to take sharing this work with a grain of salt. Stop reading when you lose interest, but welcome the churn!

Syzygies

2 tháng trướcdiscuss

Thanks for saving me the time.

I have email locally dating to the dawn of the internet; it's one form of external mind-mapping for me. I'm completely baffled that a decent mail program can't handle the mail for a small town, rather than struggling with one person's life history. This is a question of algorithm choices; performance has to be the top priority. If search is instant, who needs "features"?

Syzygies

2 tháng trướcdiscuss

There's the finished knot, and there's his way of tying it, which is easy to grasp.

That strikes a chord for me. In grade school my teachers could not distinguish between these perspectives, for the standard shoelace knot. I found their method stupid, and they thought my method was wrong. This was but one of many lessons that helped me to learn to think for myself.

Syzygies

2 tháng trướcdiscuss

Continental Airlines had an active frequent flyer community. A student emerged as a legendary figure (think "Hunger Games") after she noticed that Continental announcement URLs were numbered sequentially, and a not-yet-released announcement rather unfavorable to current elites was there for anyone to read. Quite the brew-ha-ha. Continental retreated.

She was nevertheless welcome at a frequent flyer event hosted by Continental in Houston, where she beat me at poker.

Syzygies

2 tháng trướcdiscuss

There is a meaningful design axis here, how one views one's role.

In Bordeaux, winemakers consider themselves geniuses manipulating a many variety blend. In Alsace, winemakers view their role as not screwing up God's work.

Syzygies

2 tháng trướcdiscuss

We have not yet converged on a best (or even adequate) way to present a structured mountain of information to AI, not already in its training corpus.

AI agents fielded by major AI players still fail at the basic task of providing immediate and correct support for use of the current versions of their products. If a programming language is too new to have adequate representation in the training corpus, there isn't an accepted standard way to provide a reference manual targeting AI agents. Even the best way to include documentation in a large project so new AI agents can take over is controversial. A pile of linked markdown files really isn't an answer, less structured than a codebase itself, that AI is good at navigating.

Other HN posts have discussed using SQL as a backbone for the AI "mind mapping" support we need for AI more critically than for ourselves.

I was hoping that CQL could be an answer to this. Perhaps, but not its current primary goal.

Syzygies

2 tháng trướcdiscuss

Not everyone expects to appear on HN, but chasing links this is a par two golf course:

    UFBT: Unofficial Flipper Build Tool (installation guide)

    uFBT is a cross-platform tool for building applications for Flipper Zero.

Syzygies

2 tháng trướcdiscuss

Yes, I was going to guess semantic embedding from playing around and seeing the search responses. Thank you for "About this project".

I'd love to extract just the foreign language from Pimsleur foreign language lessons, for faster review before trips. Your pipeline has many elements in common for what would be required.

Syzygies

2 tháng trướcdiscuss

I was hoping for Lean 4.

Syzygies

3 tháng trướcdiscuss

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

Syzygies

3 tháng trướcdiscuss

https://www.youtube.com/watch?v=4cia_v4vxfE

Syzygies

3 tháng trướcdiscuss

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

Submissions

Why is the California digital Covid-19 vaccine record QR-code broken?

comments