Any mathematicians looking for CS partners for the NSF proposal on AI for Math? We are thinking of doing something related to discovering relations as well as automatically formalizing proofs from both natural language and diagrams drawn by hand. We have a few other ideas too.
"We understand that a career change is a big decision. This role may even have you considering a move to Adelaide to embark on your next career chapter?"
It is a mathematical device to define what a continuous function is, in a general setting.
A topological space is a set X together with a collection of subsets of X, called open, such that finite intersections of open sets are open, and arbitrary unions of open sets are open.
A function of topological spaces is continuous if inverse images of open sets are open.
What is the intuition behind (1) and (2)?
I claim that it is better to ask, instead, how mathematicians came up with (1) and (2).
@MartinEscardo do you know, was Grothendieck's issue essentially that the Zariski topology just doesn't have very many open sets? Or was there something more to it?
What is the correct reply to a mathematician, who has never formalized anything, asking how they would go about formalizing a research paper of theirs?
@11011110@MartinEscardo@andrejbauer This is something some of us have been thinking about. We organized a reading group this semester on some potentially relevant background material.
Even for more "discrete" domains like graph algorithms, one would like to prove things about their complexity, and formalizing that complexity ultimately ends up related to some "base" computational model that needs to be polynomially related to TMs.
Formalizing TMs is a huge pain, but I don't yet know how to get around it. It'd be nice to have a "synthetic" theory of computation... I'm currently thinking to revisit some of Gurevich's writings about "what is an algorithm" in thinking about this. Would be very happy to chat about it at some point.
My experience so far has been that while categorical approaches to computation are nice in a similar way to functional programming being nice, they can be difficult to work with when one wants to do more advanced stuff with computational complexity. Maybe I just don't have enough experience working with them though...I guess we'll see.
@MartinEscardo@11011110@andrejbauer Ooh, this makes me really glad I said something here (which I was initially wavering on). I was not aware of this work, and it looks very interesting. I will definitely check it out, thanks!
@andrejbauer@MartinEscardo@11011110@yforster Yes, that's one line of research we've already been reading. Didn't realize he was on here though, thanks.
Thanks to noticing a @wikipedia edit by @11011110 on my watchlist, I realized I should see if this year's #Guggenheim Fellowships had been awarded yet. They had indeed, a week ago. So I created a list of this year's fellows, as I have for the previous two years:
@funcrunch@wikipedia@11011110 Thanks for your service! It'd be really great if that could be sorted by field, institution, etc., rather than having a separate page for each year (so at the "top level" you are forced to pick a year, rather than, say, a field, and then see all awards in that field over time). But I understand that'd be a really big table if they were all in one page. Any ideas on how to resolve this?
No one defines a #matrix as "a thing that transforms like a matrix". Why define tensors that way?
Array=numbers in a (possibly high-dim) grid
Matrix=array representation of a linear map* in a chosen basis
Tensor=array representation of a multilinear map in a chosen basis
(* or linear endomorphism, or bilinear function, but we'll get there.)
Vectors=1-tensors, but not all 1-index arrays are vectors
Matrices=2-tensors, but not all 2-ary arrays are matrices
Similarly, not all k-ary arrays are tensors. Some examples:
Christoffel symbols aren't a tensor because they aren't (multi)linear in all of their arguments.
Most "tensors" in #MachineLearning#AI aren't tensors b/c they aren't multilinear - they are just multi-dim arrays of numbers. To say an array is (or represents) a tensor is to endow it with additional multilinear structure, same as with arrays vs matrices vs linear structure.
Now, how do we get the whole "a tensor is a thing that transforms like a tensor"? Well, let's start with matrices. How a matrix changes under change of basis tells you what kind of multilinear thing the matrix is representing, and the same is true of tensors. Examples:
If a matrix M represents a linear map L:V→W, then when we change basis in V by an invertible matrix A in GL(V), and change basis in W by an invertible B in GL(W), then M changes to B M A^{-1} (where I'm writing my inputs as column vectors on the right).
In contrast, if a matrix M represents a linear endomorphism L:V→V, then when we change basis in V by an invertible matrix A in GL(V), M becomes AMA^{-1}.
If a matrix M represents a bilinear map V⊗V→F (by (x,y)→x^t M y), then under change of basis A^{-1}, M becomes A^t M A.
e.g. if I tell you I have a matrix M and under change of basis it transforms as A^t M A, then I know it's representing a bilinear map of the form V⊗V→F. etc.
Similarly, if I tell you what kind of multilinear "thing" a tensor T is representing, then that tells you how it transforms under change of basis, and vice versa. For 3-tensors, there are several natural possibilities (up to permuting indices):
U⊗V⊗W→F
U⊗U⊗V→F
U⊗U⊗U→F (trilinear map)
U⊗V→W (bilinear map)
U⊗U→V (bilinear map)
U⊗V→U (linear action of V on U)
U⊗U→U (algebra, not nec. associative)
U→V⊗W
U→U⊗V (coaction)
U→U⊗U (coalgebra, not nec. coassociative)
F→U⊗V⊗W
F→U⊗U⊗V
F→U⊗U⊗U
@mrdk I don't think so (you can define linear transformation etc. without choosing a basis, but a matrix involves a choice of basis), but I see your point.
where he says "tensor" is the generic term for multilinear things, and "hypermatrix" should be what I called "tensor" in this thread. Maybe I agree w/ that!
I don't think it is unreasonable to demand confidence from a proof assistant. But some people seem to be saying it is fine to live without the confidence. I am very puzzled about this.
@MartinEscardo While I don't share their opinion, I can imagine it. Not everyone wants proof assistants to add confidence, some people just want them as tools that aid in finding proofs. Similar to how many people currently use computer algebra systems (but in a different way/domain).