Choose your own adventure (redux)

Apr 16 2020, 12:39

I've decided to design a small "choose your own adventure". For fatalists. You can also play the interactive version here!.

This was originally "in-blog", but I decided that the interactive version is a bit more interesting. Enjoy it while it lasts!

Some thoughts about "automated theorem searching"

Jun 27 2016, 01:02

Let me begin by giving a spoiler warning. If you haven't watched "The Prisoner" you might be spoiled about one of the episodes. Not that matters, for a show from nearly 40 years ago, but you should definitely watch it. It is a wonderful show. And even if you haven't watched it, it's just one episode, not the whole show. So you can keep on reading.

So, I'm fashionably late to the party (with some good excuse, see my previous post), but after the recent 200 terabytes proof for the coloring of Pythagorean triples, the same old questions are raised about whether or not at some point computers will be better than us in finding new theorems, and proving them too.

Iterating Symmetric Extensions

Jun 22 2016, 07:43

I don't usually like to write about new papers. I mean, it's a paper, you can read it, you can email me and ask about it if you'd like. It's there. And indeed, for my previous papers, I didn't even mention them being posted on arXiv/submitted/accepted/published. This paper is a bit different; but don't worry, this is not your typical "new paper" post.

If you don't follow arXiv very closely, I have posted a paper titled "Iterating Symmetric Extensions". This is going to be the first part of my dissertation. The paper is concerned with developing a general framework for iterating symmetric extensions, which oddly enough, is something that we didn't really know how to do until now. There is a refinement of the general framework to something I call "productive iterations" which impose some additional requirements, but allow greater freedom in the choice of filters used to interpret the names. There is an example of a class-length iteration, which effectively takes everything that was done in the paper and uses it to produce a class-length iteration—and thus a class length sequence of models—where slowly, but surely, Kinna-Wagner Principles fail more and more. This means that we are forcing "diagonally" away from the ordinals. So the models produced there will not be defined by their set of ordinals, and sets of sets of ordinals, and so on.

What I realized recently

Mar 30 2016, 18:04

I recently learned that diamonds are cut and polished with the dust of other diamonds. And I recently realized that success is cut and polished with the dust of failures.

In particular a successful mathematical idea is polished with the dust of the many failed ideas that preceded it.

The rules of research

Jul 08 2015, 03:27

Here are the rules of research. Feel free to add your own.

1. If it seems obvious, it's probably false as stated.
2. If it seems obvious and true, it's probably false without additional hypotheses.
3. If you think that you wrote a proof, you probably missed something obvious. See (1) and/or (2).
4. You missed something obvious, see (1).
5. When you go to see your advisor, suddenly all your thoughts align, and you find the solution.
6. Two hours after finally talking with your advisor, you realize that your solution is obvious, therefore (1) or (2) apply.
7. If you use forcing to prove the argument, then you probably missed some object being encoded generically.
8. If you use forcing, and you didn't miss some crucial object, then you missed some other crucial object not being coded by the generic.
9. When the truth is found to be lies, and all the joy within you dies...
10. It's not false if you can force it.
11. It's not true if you used the axiom of choice more than three times in the proof.
12. It's not cheating if you asked a visitor to the university whose visit did not span longer than two weeks from the moment you asked them.
13. If your question was about inner models, you may extend the above timespan to a month. Equally, if the question is about the axiom of choice, it should be shortened to a week.
14. It's not considered unethical to make sacrifice in order to appease Mayan and Aztec gods. Just in case we got it wrong, and they're in charge of the mathematical universe.
15. If it still seems obvious, you're probably right. It's still false, though.
16. If you need six technical lemmas, whose proof is reduced to a single line (or just one lemma with an actual proof), then it's probably obvious. Unfortunately, see (1) and (2).
17. If by some chance something is obvious, but you wrote out the proof, and it checks out, then it wasn't obvious at all.
18. Remember what the dormouse said: feed your head.
19. If you haven't watched Futurama in a while, then you're doing something wrong.
20. Whatever happens, it's the other guy's fault. Also, see (1).
21. I just work here, you know? I don't.
22. Rolling a D20 die to determine the truth value of a statement is the original algorithm behind proof verification software.
23. When you hit the wall, and you're about to give up and decide that whatever you're trying to prove is false, see (4).
24. The only proofs that write themselves are obvious proofs. If your proof is obvious, see (2) and (3).
25. To be honest, it needs more cowbell.
26. Seriously, you're gonna want that cowbell in your proof.
27. See (1), (2) and (4).

The Torture of Mathematical Research

Apr 22 2015, 08:12

In a manner more befitting to Edgar Allan Poe, Mathematics is a cruel and unforgiving mistress.

Mathematics will often dangle in front of you some ideas, and you will work them out, to find a mistake. Then you will go back to the beginning, find new ideas that she had in store, work those out and proceed only to find a mistake much later. Then you go back to the beginning, and you find yet another minor idea that was missing, and now when everything works you continue. But then you find another gap, and you have to go back to the beginning and hope to find yet another idea. And don't get me started on those ideas that you find not to work during all these searches.

Existentialism II, like Colonel Kurtz

Mar 11 2015, 00:34

Last night I posted a strange story about a gecko and a moth.

It occurred to me today that this is a very Kurtzian story, if we take the Brando interpretation of Mistah Kurtz (he dead) in Apocalypse Now! (the Redux version is one of my favorite movies, I guess). In the movie Harrison Ford plays a tape where Kurtz is describing a snail crawling along the straight edge of a razor, crawling slithering, this is his dream, this is his nightmare.

Existentialism

Mar 10 2015, 00:34

Spring has begun in Israel.

Yesterday was the first day where you could say that the weather is characteristically spring; and today (as well tomorrow) we are expected for a daytime heatwave and a nighttime cold weather (e.g. Beer-Sheva is expecting a whopping 31 degrees centigrade during the day, and 13 during the night).