please send me an email <siddu.druid@gmail.com>. I'm a PhD student at cambridge, and might be able to put you in touch with folks who have positions to hire you as an RA if your research profile fits. even if there isn't an immediate fit, I'm happy to scout around and see if anything pops up. Best, Sid
Having similar reasoning, I would up writing a tiny-optimizing-compiler tutorial that only explains how to write a middle and back end of a compiler: https://github.com/bollu/tiny-optimising-compiler
yes, Lean is executable, and the proof of natural numbers runs with arbitrary width integers. they're stored as tagged pointers, with upto 63bit numbers being normal numbers, and larger numbers become GMP encoded.
How does one formally define a spinor? I've seen the definition of a spinor field as "things that transform like a spinor", and a spinor as a "representation of the spin group" (which representation), but I would like to know a canonical mathsy definition of what the heck a "spinor" is! May I please have one? :)
Unfortunately there are slightly different but related notions of what spinors are. One key idea is indeed how they transform. A spinor ψ transforms with a transformation S ∈ Spin(n) in a one-sided way: ψ -> Sψ. A vector v in contrast transforms in a sandwich way (with the inverse on one side): SvS^-1. Intuitively this explains why spinors transform "half as much" as vectors, e.g. the 720° vs 360° rotational symmetry that shows up in physics. So for any S ∈ Spin(n) the sandwich-action (S|S^-1) gives you the corresponding element of SO(n). Because a negative sign on S squares away in that case, S and -S map to the same SO(n) action, and therefore Spin(n) is said to be the double-cover of SO(n) (personally I think it would be better terminology to call SO(n) the half-cover of Spin(n)).
So a spinor could be said to be anything whose symmetries are a Spin group. Spin groups are easily constructed in clifford algebras and it turns out that they have matrix representations. Whenever you have matrices (linear maps) you may wonder what the vector space is that they act on (i'm now using the term "vector" abstractly, not in contrast to spinors as above). Well, those are the spinors (technically pinors)! Another definition of spinors is that they live in a minimal left ideal of a clifford algebra. This does not sound very intuitive at first, but it can be understood easily as simply taking the matrices with only one non-zero column. These are really not very different from colunm vectors then.
There seems to be some confusion about pinors and spinors in that perspective though...it just seems to be a somewhat confusing concept in general.
The spinors/vectors relevant to the article are those of Spin(8), which has something to do with triality (still need to understand all of this better myself). The basic idea is that in Cl(8) the vectors and spinors are both 8-dimensional and the algebra can be generated by left-multiplication of octonions. So there are some interesting symmetries occurring. The Baez-article goes into that too but it could have been a bit more explicit for my taste.
I hope some of that made sense, i don't know your background. I'm still trying to wrap my head around this topic myself and have been for about 2 years now.
Maybe check out the "spinors for beginners" series on youtube. It's very good and quite extensive.
> The spinors/vectors relevant to the article are those of Spin(8), which has something to do with triality (still need to understand all of this better myself).
Spin(8) itself doesn't have much to do with triality; it's just that triality describes an unusual symmetry among representations of Spin(8), due to an unusual outer automorphism. (Of course, from some perspectives, that means that Spin(8) has everything to do with triality, but I hope my meaning will be clear.) The best accessible mathematical explanation of triality I know is from Baez: https://math.ucr.edu/home/baez/octonions/node7.html.
> So a spinor could be said to be anything whose symmetries are a Spin group. Spin groups are easily constructed in clifford algebras and it turns out that they have matrix representations. Whenever you have matrices (linear maps) you may wonder what the vector space is that they act on (i'm now using the term "vector" abstractly, not in contrast to spinors as above). Well, those are the spinors (technically pinors)!
One has to be a little careful here, because algebras have lots of representations, and there's no one representation that a priori may be said to be "the vector space on which they act" ("the" rather than "a"). For example—though it's a bad example because it's not a faithful action—Spin(8) naturally double covers SO(8), but we don't want to take the resulting 8-dimensional orthogonal representation (the "vector representation"). Instead, we want to take one of the three fundamental representations permuted by the triality automorphism (the V_1, V_2, V_3 in Baez's article).
I slightly edited my post while you were writing yours. I'm aware of the article but I still think it could be clearer. I'm a big fan of constructive proofs but that does not seem the case for most mathematicians, so i find a lot of stuff in math very unsatisfying and have to rediscover it myself via different routes. Educational for sure but not always so easy.
How come "representation of the spin group" is an insufficient starting point?
Spin group seems like they either have a specific group (from Algebra) in mind or that spins are at least defined by choosing a specific group (a set with a binary operation satisfying the group axioms/definition).
A "representation" also has a definition in Algebra with regards to groups. There are group homo-morphisms between two groups. This means you have a mapping that preserves group structure. Representation theory is about mapping groups into the set of matrices or a subset of matrices "with numbers in the matrices." Then there are group actions (don’t care for the name) - basically/conceptually a set of functions that behaves like a specific group under composition, but way more notation around that. Finally, category theory looks at "groups of groups" with the binary operation being homo-morphisms between the "inside/smaller/contained/internal" groups thus forming a larger "outside" group called a category. Because this involves talking about sets of sets you end up also needing the term "class" from set-theory.
It's not that "representation of the spin group" is undefined, but that there are too many of them for it to pin things down uniquely. (In this case, fortunately, it's not hard to say which representation it is (see https://news.ycombinator.com/item?id=43388052), but just saying "a representation" isn't enough.)
While we're talking about representations, there's something I've always wondered. Why are the objects that the maps which are the representations act on also called representations? Spinors don't act as the spinor group, S ⊂ Hom(Spinor,Spinor) does.
> While we're talking about representations, there's something I've always wondered. Why are the objects that the maps which are the representations act on also called representations? Spinors don't act as the spinor group, S ⊂ Hom(Spinor,Spinor) does.
Physicists and mathematicians speak differently, but I think that mathematicians usually avoid this language. For us, spinors are elements of the spinor representation, and, more generally, the things on which a representation acts are called generically "vectors in the representation", not representation themselves.
(That said, one will often see in math language like "let V be a representation of G", meaning more formally "let G \to GL(V) be a representation", which probably is the sort of abuse of language you mean.)
> How does one formally define a spinor? I've seen the definition of a spinor field as "things that transform like a spinor", and a spinor as a "representation of the spin group" (which representation), but I would like to know a canonical mathsy definition of what the heck a "spinor" is! May I please have one? :)
For Spin(8), three of the four fundamental representations are conjugate, and so we can use any one of them to define spinors.
> there’s no shortcuts. I have to be able crawl, then walk, before I can run.
yes, so much this!
my.fad, also a passionate artist, hated how they thinned out technical crafts foundations from arts college. "no more stupid copying and banale Line and color practice! freedum!" the college went.
my dad just said (translation follows)
@> Kunst kommt von können. Wenn es von wollen käme hieße es Wunst und wir wären Wünstler.
art comes from artistry. if it was based on "wanting" we'd call it "want" and we (artists) were "wantists"
or "wished" and "wishedits"
along these lines
he'd learned sketching from herding small livestock, goats, geese, chicken and sketching them, as a kid...
ChrisMarshallNY gave you the true answer, as far as creating the type of art that he's made (which I find amazing) and mastering painting. Another way to go about it (which I did at the start of the pandemic) is to just buy some canvases and acrylic paint (more forgiving than oil since you haven't painted), and some cheap brushes. Experiment and try to create something. It can be completely abstract and only for you. Learn how the paint dries, and how adding a bit of water to your paint affects it. Look up some YouTube tutorials on beginning painting. Best thing to do is to just keep painting. You can even take a canvas and just keep painting white or black over it to start over, just so you aren't spending much on canvas. I am totally unable to paint 3D objects, but I do a lot of abstract and symbolic/occult type art, and I personally love it as a means of meditation and getting away from technology.
There are a large number of courses for both digital and traditional painting on platforms like Udemy, many of which are insanely good value when they go on sale.
I'm curious, which solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean (https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%...), and it's genius --- the algorithms, the reductions, the heuristics, it's all so deep.
I like the definition proposed in the post - all possible mazes should be equally likely. A function could return the same maze each time and pass the criteria above.
reply