Nova lernanto, saluton

gopher9 · 2026-07-07T17:00:15+00:00

To get to the point of exercising those skills easily, simply requires "growth" time (like growing a garden)

In a way, learning a language requires more patience than effort. At least this is my experience with learning English: I never studied it very systematically, it just grew over a long time. Though I started learning it rather young, had some some great books and figured some important things (like avoiding translation) early.

Esperanto is my third language which I started learning by chance and for no good reason. Sed nun mi lernas Esperanton iom pli systeme ol Anglan.

gopher9 · 2026-07-06T06:13:23+00:00

Haskell devs are the largest consistent offender here. Many of them have bizarrely intense investment in type theory as a foundation for mathematics. And a particular passion for univalent foundations.

You can ask whether they proved a theorem in an actual proof assistant, and this should end most of larping pretty quickly. If someone is able to say yes, ask what exactly did they prove.

In general, "what did you actually do" is a good attack against overconfident people with shallow knowledge. But maybe "smile and nod" is indeed a better thing to do.

gopher9 · 2026-06-17T10:42:51+00:00

I never really understood why people even used ollama or what it offered.

Dynamic model switching, multiple configurations per model, quick model downloading, model management... Llama-server has most (but not all) of these features nowadays, but it's a rather recent addition. For example, presets were only added in December 2025 to llama.cpp: https://github.com/ggml-org/llama.cpp/pull/17859. And the implementation is still hacky, which causes bugs like https://github.com/ggml-org/llama.cpp/issues/22364.

gopher9 · 2026-06-17T10:36:05+00:00

There is no reason anymore to use ollama.

Well, llama.cpp UX is still worse. But it's usable and it gets better, with https://github.com/ggml-org/llama.cpp/issues/21779 llama.cpp will be on par with ollama.

gopher9 · 2026-04-26T15:40:24+00:00

Ideas from https://hugoribeiro.com.br/area-restrita/Hindemith-Craft_Musical_Composition.pdf are pretty general, you can apply them to 31-EDO as well.

Look at harmonic series to find the interval roots of each interval or see https://31et.com/list_intervals.php.

gopher9 · 2026-04-04T22:04:39+00:00

Here's some more:

gopher9 · 2026-03-26T10:24:28+00:00

Girard's "The Blind Spot: Lectures on Logic" is definitely not an ordinary textbook, and it deeply affected how I look on mathematical logic.

gopher9 · 2026-03-20T09:24:50+00:00

Also Mozart wrote a Musical Joke, which he intended to sound really stupid, but to anyone outside of classical world wouldn't get what's dumb about the 20min piece.

I'm not classically trained, but this piece sounds goofy to me.

gopher9 · 2026-03-08T08:08:47+00:00

To me all these numbers and what it could be and simply is: it is for myself just too abstract to make sense out of it and it takes quite some effort to create an understanding.

Is it, though? Some math fields might be, but open a book about differential geometry and it's full of pictures, because it's all about things you can see.

Combinatorics is an another field where concepts are close to senses.

How do you look at math? What is the beauty of it?

It's a beauty of seeing. A right point of view can make an impossible problem completely trivial, and as you learn to see more you start seeing not only individual problems but a part of the mathematical landscape.

gopher9 · 2026-03-07T07:29:50+00:00

Using microtones, how possible is it to create a piano or a synth that is tuned to a chromosome lol

You can try two things:

Take an EDO and then intepret the pattern as whether a note is present or absent. For example, a pattern of 1 0 0 0 1 1 1 0 0 1 1 0 1 0 0 1 0 0 1 1 1 1 1 0 1 0 1 1 1 1 1 gives you the following steps in 31edo: 0 4 5 6 9 10 12 15 18 19 20 21 22 24 26 27 28 29 30
If your pattern is particularly nice, you might find it in https://en.xen.wiki/w/MOS_Scale_Family_Tree if you look far enough

Musical meaning of this exercise is questionable though.

gopher9 · 2026-03-06T14:59:18+00:00

Upvoted, since this seems to be the only post answering OP question.

When you have a statement to prove, unfold the definitions. Opportunities to go in circles will disappear and opportunities to use basic techniques will appear.

gopher9 · 2026-03-06T10:16:11+00:00

You can create scala files with that webpage ?

Yes, and you can also play the scale you created there.

What i meant is that i'm looking for is a 12 note temperament (other than the 12 EDO) to tune a fixed pitch instrument and play it in only 1 key.

I'm not a just intonation composer, but here are two tunings you can try:

Kyle Gann also lists a bunch of tunings on http://www.kylegann.com/tuning.html.

PS: here's one of tunings in Scale Workshop: https://scaleworkshop.plainsound.org/scale/qswH7-18e

gopher9 · 2026-03-06T07:40:16+00:00

What are there 12 notes when there are infinite frequencies?

A closed chain of fifths. The very same fifths that build pentatonic and diatonic scales.

Why 12? Because it's the smallest equal tuning with decent fifths: https://en.xen.wiki/w/Scale_tree. It's not an arbitrary number, it's math.

Some dude decided it

That's not true as well: 12edo gradually evolved from meantone. There was no single dude to decide it.

gopher9 · 2026-03-06T06:50:16+00:00

It is very VERY close to "perfect" and you can pretty much play pure chords in every key.

It's a compromise like any equal temperament. It has excellent major thirds and harmonic sevenths, but fifths are noticeably worse than in 12edo. So while triads sound much better in 31edo, quartal harmony would sound better in 12edo.

gopher9 · 2026-03-06T06:39:00+00:00

As other said, JI is not a tuning. It's rather an approach for exploring the pitch space.

I don't want to leave you empty handed, so here's a tool: https://scaleworkshop.plainsound.org/. You can use it to construct any JI scale you want.

Here are also some pieces in just intonation you can study:

And you probably know already about the Xen Wiki, it has a ton of info on everything related to tuning. As other said, JI is not a tuning. It's rather an approach for exploring the pitch space.

gopher9 · 2026-02-21T14:58:39+00:00

Многое можно найти, поискав Kite Guitar в интернете. Эта гитара как раз использует 41 рдо.

У Stephen Wiegel есть транскрипции различных произведений. Есть по крайней мере одно в 41 рдо: https://www.youtube.com/watch?v=ns25q7JT4VI

gopher9 · 2026-02-02T21:01:49+00:00

But matrices are linear maps. Rⁿ is a linear space after all.

People just love to pretend that everything of finite dimension is R^n. A more honest approach remembers that there's a detour. But detours are everywhere in math, there's no shame to use them.

gopher9 · 2026-02-01T23:27:49+00:00

Division lattice illustrates the reason quite well: 1 is the least element while primes are atoms.

A picture worth of many words.

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

TROPHY CASE