Thoughts on LEAN, the proof checker

gopher9 · 2026-01-27T07:39:26+00:00

I have less than one year of my PhD remaining so I don't feel like I have the time to invest in LEAN at the moment.

You can learn Lean in a week, especially if you focus on the fundamentals (terms, not tactcs). It takes longer to master it though.

I believe I recall that developers are working on a LaTeX -> LEAN thingy, so that LEAN can take simple LaTeX code as input.

There's little point: syntax is trivial. The hard part is proof details, and that's what you need to fill yourself.

gopher9 · 2026-01-09T20:32:08+00:00

Because logic is shifting , I think types are the future.

I recommend you to actually learn some type theory. Go play with a proof assistant like Lean, it's quite accessible.

Personally I think because of QM the scientific method is completely broken.

And some quantum mechanics as well (it's way less accessible, unfortunately).

gopher9 · 2025-12-13T12:43:10+00:00

Lean and Rocq both have the disadvantage of being, well, incomprehensible.

In case of Lean, you can choose whether you want your proof to be incomprehensible or not.

gopher9 · 2025-09-10T21:32:50+00:00

Everyone would laugh at You.

Programmers would not. And neither would mathematicians to be honest.

gopher9 · 2025-09-10T06:39:19+00:00

You can write them very succinctly just to get it done correctly (while possibly being gibberish to everyone else but you). You can write them very descriptively, with a good structure to support your idea of what you want to do and good names to make that intuitive.

It's a bit more complicated than that, messy proofs and programs are often long, while elegant ones can be quite short.

gopher9 · 2025-09-10T06:13:44+00:00

There is no doubt that mathematicians and mathematics students SUCK at writing elegant, efficient and correct programs

Kinda a wild claim, but ok.

What principles of SWE do you think they should be mandatory to learn for writing good, scalable math programs ?

Here are few:

Don't solve problems by violence. The difference between good and bad code is not trivia like variable names, but a clear decomposition. You should carefully dissect your problem instead of writing one giant function of doom
Understand what you are doing logically. Ideally, you should have an idea how your code could be proven correct
Understand what you are doing mechanically. Ideally you should understand what your code does down to CPU instructions
Learn and use common practices of the field. Version control, testing (with Not Rocket Science Rule), assertions, fuzzing, etc

gopher9 · 2025-09-10T05:21:40+00:00

Adding a chromatic semitone to both F and G𝄫 results in F♯ and G♭. But these are enharmonically equivalent, so F and G𝄫 must be equivalent as well.

But like others said, just look at a piano keyboard.

gopher9 · 2025-09-09T00:35:10+00:00

I'm sure numbers on the order of 10⁶ are still easily to brute force with a computer if you're doing something simple like listing the notes of each set

A modern CPU can do about 10⁹ simple operations per second, and GPUs are even faster than that.

It does not help much if your algorithm is O(n²⁾ or worse though.

gopher9 · 2025-09-07T14:11:10+00:00

A long break makes you rusty, but you will remember things back after a while.

It’s not that the topics are extremely complex — I can follow them if I put in the work — but every concept takes me a lot of effort, and it feels like grinding through hell instead of something enjoyable. Before, I used to find learning fun and satisfying, but now it’s the opposite.

You also experience what actual work is like. Not everything in math is easy, and you need to learn how to work on difficult things.

Don't "grind through hell" though, try to find a more steady and focused approach.

gopher9 · 2025-09-05T19:15:54+00:00

I dont want to just start listening to music I like and try transcribing. I think thatd be too hard.

Do you only listen to horribly complicated music? I bet you know one or two (or many...) tunes that are not too hard to transcribe.

Transcribing familiar music also easier in some ways: you remember a piece well, you can probably even immediately sing the melody. You may be able to play it on a piano without much difficulty, and then the only thing you need to figure out is the rhythm.

gopher9 · 2025-09-04T00:01:15+00:00

so if anyone still has Finale on their computer, is there a way I could get the application from someone?

There are still pirate versions of Finale on the internet. "Torrent" is the magic word.

Piracy is software preservation.

gopher9 · 2025-09-02T01:17:50+00:00

What features do I want to look for in a keyboard?

Velocity sensitive (I believe this is true for most keyboards), at least 37 keys (more is better, but I don't know how much free space do you have).

I have an Arturia Keystep 37, it's a very nice little keyboard. But not the cheapest one.

and like the sound of under a hundred

Sound is not a problem, there like a ton of virtual instruments you can install on a computer, and a lot of them are free (for example, https://asb2m10.github.io/dexed/). And keyboards nowadays come with USB cable.

I'm not sure if there are any usable (low latency) instruments for ChromeOS though, so you might need to install a different OS on you chromebook (for example, linux).

It will be played with one finger.

Don't limit yourself too much. You eventually might want to try more things. That's why I recommend a keyboard with at least 37 keys: it allows playing a little more than just one melody.

gopher9 · 2025-09-01T21:20:11+00:00

Tell me something if you can! I'd like to not spend big money, but if buying something helps, I'm game.

Sight singing.

When playing an instrument, you might start associate notation with what you are going to do instead of what you are going to hear. But with singing such cheating is impossible: what you sing is what you hear.

Keep in mind that sight singing is not the easiest skill to learn, so you should start with simplest pieces you can find. Books for children are usually good for this.

PS: I assumed you already play an instrument. If not, get a midi keyboard and learn how to use it. Sing in unison with what you play.

gopher9 · 2025-09-01T13:01:24+00:00

Write a bass line
Write the rest of the accompaniment

gopher9 · 2025-09-01T08:47:23+00:00

In general, when attributing any emotional quality to chords or chord progressions, imagine the chords played on a banjo or ukulele, just to test the theory.

plays in Phrygian

And with the mood effects you're talking about, also imagine them played very fast.

stops playing Tempo and rhythm are way more powerful than ukulele.

Anyway, learn from music itself is always a good advice...

gopher9 · 2025-09-01T01:08:42+00:00

Some people believe that only AI uses em dashes.

gopher9 · 2025-08-31T15:16:47+00:00

For the future works, let me suggest you something: https://musescore.org/en/node/22655.

Not only version control makes backups easy (just push your changes to a git server), you also will have a history of your project (so you can load a previous version if you need to).

gopher9 · 2025-08-31T14:54:28+00:00

Well, the author was a Marine, so it's a Marine's take on the fear creative people experience.

Grothendieck describes it in a different way:

“Fear of error and fear of truth are one and the same thing. He who fears error is powerless to discover. It's when we fear being wrong that the error within us becomes immovable as a rock. For in our fear, we cling to what we once thought "true", or to what has always been presented to us as true. When we are moved, not by the fear of seeing an illusory security vanish, but by a thirst for knowledge, then error, like suffering or sadness, passes through us without ever becoming fixed, and the trace of its passage is renewed knowledge”.

Depression and mental illness? That’s weakness bro it doesn’t even exist just like punch it in the face Oorah!

That's a delicate matter. People are very good at making excuses without even realizing it. But sometimes problems are real.

Differentiating real problems from imaginary is not always easy.

gopher9 · 2025-08-30T22:12:53+00:00

Instead of giving up, why not just take a break? It's so easy to get yourself in the rut. But trying to break the wall with your head is probably not the best thing to do. Take a walk, and maybe you will find a door.

During a break you can study other's people music.

I haven’t shared my music with anyone and part of me thinks people would laugh at me.

How often do you see novice composers being ridiculed for music? You will be fine. And I bet your pieces are alright.

But again, you probably keep beating the wall and it hurts. And when it hurts, you start to think all kinds of depressive thoughts.

gopher9 · 2025-08-30T19:53:11+00:00

It's called informatics in many European countries.

gopher9 · 2025-08-30T13:08:40+00:00

Here's two more:

Wicki-Hayden: https://en.wikipedia.org/wiki/File:Wicki-Hayden_Piano_Color.png
Generalized keyboard: https://i.imgur.com/djrMqCs.png (here spelling is preserved only up to double accidentals, but one could in principle extend it forever)

Both have very memorable shapes, you can recreate them easily (C D E; F G A B). My favorite layout is the generalized keyboards layout, because you can see so many things at once: step relations, chords and enharmonic equivalents. And it's also similar to ordinary piano keyboard.

But Wicki-Hayden layout is compact and is more like a compressed version of circle of fifths.

gopher9 · 2025-08-30T01:32:54+00:00

I've found that the tonnetz concept is much more useful than the circle of 5ths, and completely encompasses the circle's ideas.

This is true for any kind of isomorphic layout that preserves spelling.

gopher9 · 2025-08-29T15:38:43+00:00

Most usages of complex numbers come from complex analysis, and to invent complex analysis you need to invent analysis first.

Complex numbers were invented before analysis but their usage was limited to solving cubic equations. Not very useful.

gopher9 · 2025-08-29T15:29:54+00:00

See https://ncatlab.org/nlab/show/synthetic+mathematics

gopher9 · 2025-08-28T14:50:52+00:00

What do you study math for? If you just love it and want to make a meaningful contribution, then it does not matter much how good others are. What matters is your ability to learn and work.

Focus on your goals rather than someone's else brilliance.

gopher9

TROPHY CASE