52

I will stay away from the academic politics of hiring "professors of data science", but if I interpret the question more specifically as "does data science offer problems of mathematical interest", I might refer to Bandeira's list of 42 Open Problems in Mathematics of Data Science. (The full list from 2016 is here, and Bandeira's home page links to ...


44

Using the $\Delta^2- \epsilon \Delta$ approach, Tim Netzer and I have verified Kazhdan's property (T) for ${\rm SL}(3,\mathbb Z)$. For the standard generators $e_{ij}$ ($i\neq j$) we can show a spectral gap of the normalized Laplace operator of $1/120$. There is a lot of room for further improvement. To my knowledge, the best previously known lower bound ...


41

The short answer is that there are no implications. As Scott Aaronson said on his blog, the fact that even a polynomial time algorithm for GI has no implications for complexity classes is one reason some people conjectured that GI might be in P. He continued: In fact, the main implication for complexity theory, is that we’d have to stop using GI as our ...


37

I don't think there is any compelling evidence that integer factorization can be done in polynomial time. It's true that polynomial factoring can be, but lots of things are much easier for polynomials than for integers, and I see no reason to believe these rings must always have the same computational complexity. (Strangely, if you do believe that, it ...


31

The Mathematics of Data may go some way towards answering your question. As one example of a mathematically interesting topic that is motivated by data science, you might want to look at the concept of persistent homology.


31

Fundamentally a lot of what a modern data scientist does is very similar to what in previous generations would have been the responsibility of a statistician, and it shouldn't surprise you that there are professors of statistics. Mathematically there are quite a few interesting things that come up in a lot of modern data science, but first let me make a non-...


30

I can make a little progress here. One of your key subproblems is: Given a computable group $G$, a finite list of elements $T \subseteq G$ and an element $\alpha \in \mathbb{Q}[G]$, determine whether there exist $\xi_1$, $\xi_2$, …, $\xi_k$ in $\mathbb{R} T$ so that $$\alpha = \sum_{i=1}^k \xi_i \xi^{\ast}_i.$$ This problem can be solved by semidefinite ...


29

Yes, there is a whole research area devoted to this problem -- it's called "implicit complexity theory". The general idea is to use a lambda calculus based on linear logic. The linearity constraint on lambda-terms lets you control the complexity of cut-elimination (and hence of evaluation), giving natural programming languages that are complete for various ...


28

Because there are natural computational problems involving many mathematical objects, there are a bunch of implications of complexity class separations like $\mathrm{P} \neq \mathrm{NP}$. I think the first paper to investigate this idea is probably Mike Freedman's Complexity classes as mathematical axioms, which assumes a complexity class separation (namely $...


25

Briefly, this works very nicely when $X$ is locally compact, but not otherwise. Then the function space carries the compact-open topology. John Isbell gave a survey of the story and literature in his paper General Function Spaces, Products and Continuous Lattices, in Math Proc Cam Phil Soc 100 (1986) 193--205. It is an ongoing matter in theoretical ...


25

Here is one way of interpreting your question. In my joint paper: Joel David Hamkins and Alexei Miasnikov, The halting problem is decidable on a set of asymptotic probability one, Notre Dame J. Formal Logic 47 (2006), no. 4, 515--524. blog post, the main theorem is that for some of the standard models of computation, the halting problem is decidable with ...


24

As you noticed in your question, for any particular value of $n$, there is a constructive algorithm that solves the halting problem for instances of size at most $n$. Since for a particular value of $n$, there are only finitely many instances, one may simply hard-code the finitely many answers into the program itself. So in this sense, yes, for any ...


23

I am going to answer the question as if you asked about massive formalization of proofs, not automatic extraction of formal proofs from existing informal proofs written in books, because that's a fairly hopeless task. One of the major lessons learned by Gonthier et al. was that published proofs rely on large amounts of implicit knowledge that is ...


22

Much of the early work on the Mandelbrot set was of this type. You see something strange in the computer images, then you try to prove that it really happens. Here is one example: Pi and the Mandelbrot set. From conjecture in 1991 to paper in 2001.


22

My attempt to do something like this for Agda is here: http://neil-strickland.staff.shef.ac.uk/formal/. I would also like to see a Coq equivalent (also Isabelle, Mizar etc) but I do not currently have the knowledge to write one myself.


22

I think Andrej's opinion is very accurate. Here are a few more comments based on my experience as a contributor to the Coq proof of the Feit-Thompson theorem (sorry it's a bit long). This formal development comprises three natures of libraries: some are for infrastructure purposes and no mathematician cares about the lemmas they prove (litanies of lemmas on ...


22

The 1/3-2/3 conjecture is probably considered one of the most significant open problems about finite posets; see the Wikipedia page: https://en.wikipedia.org/wiki/1/3%E2%80%932/3_conjecture.


20

Dear Ronnie, The example you refer to (April 22) uses the idea of a placement of a body B in an environment E, and notes that a path in the space of placements corresponds uniquely to a placement of B in the space of paths, because both correspond to a lower-order map from IxB to E itself. These correspondences are invertible, as well as smooth, recursive, ...


20

I think it is appropriate to let MO users know (the OP himself knows it well) that this question was recently solved: it is feasible to provide a computer based proof for property (T) using the Ozawa Equation and this method was applied successfully to the groups mentioned in the question. In particular, the famous open problem alluded to above is now solved....


20

One can use the Dirichlet hyperbola method to compute $\sum_{i \leq n} \sigma(i)$ in time $O( n^{1/2} )$ (up to logarithmic factors coming from arithmetic operations such as division): \begin{align} \sum_{i \leq n} \sigma(i) &= \sum_{i \leq n} \sum_{d|i} d \\ &= \sum_{d,m: dm \leq n} d \\ &= \sum_{d \leq \sqrt{n}} d \sum_{\sqrt{n} < m \leq n/...


20

This conjecture is false, though only barely. It should be true for $N_0 \geq 4$ by the ABC conjecture. But for $N_0 = 3$ there are infinitely many counterexamples such as $$ 191114642^3 + 4309182809^3 = 7^4 \, 321817873^3. $$ I obtained this by starting from the point $P_1 = (2:1:1)$ on the elliptic curve $x^3+y^3=7z^3$ (with origin $P_0 = (1:-1:0)$), ...


19

Lovasz told me the following interesting story. He had read a paper containing a long list of computer generated conjectures, did not like most them, but suddenly found one, which turned out to be an interesting and deep question. Then he realized that the same question had been asked earlier by humans. See http://oldwww.cs.elte.hu/~lovasz/berlin.pdf.


19

Here is an example of the type you appear to be seeking. The story -- like many good stories -- involves a million dollar prize offered by a billion dollar corporation, sought by armies of computer wizards. There's even a courtroom scene at the climax. In 2007, Netflix released a dataset consisting of roughly a hundred million movie ratings (from 1 through ...


19

It's simple. If the halting problem is undecidable, then PA is not complete, since otherwise, you could solve the halting problem by searching for proofs in PA. And the same argument works for any sound computably axiomatizable theory $T$ able to express arithmetic. Given a Turing machine $M$ on input $i$, you formulate the assertion $\sigma$ asserting that $...


18

I imagine the seminar exercise went something like this. Let $M$ be a winning machine with starting state $A$, halting state $H$ and one other state $B$. Let's build the transition function of $M$ (or an equivalent or better winner) by looking at the first few transitions. We can assume the first transition is: $(A, 0) \mapsto (1, R, B)$ because, (a) if $...


18

Answer from Yury I. Manin: 1) I understand (semi)computable functions as (partially) recursive functions; so arguments and values are from the start natural numbers. But they can be also rational numbers, finite words in a finite alphabet and a lot more: cf. Chapter V of [1], and also pages 285-296 there. 2) The exponential Kolmogorov complexity of a ...


18

There are logical systems whose formal proofs are not computer verifiable. One such example is infinitary logic in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not ...


17

I believe the explicit use of definitions by primitive recursion goes back to Grassman, 1861. Dedekind in 1888 not only highlighted such definitions but had a proof that they work as intended, i.e. define unique functions. But it is probably Skolem who first clearly recognised the primitive recursive functions as together forming a class of functions of ...


17

Let us assume that everybody uses the same asymmetric encryption system (such as PGP), with keys that are so large that Big Brother cannot crack them. If Alice wants to send a message to Bob, she encrypts it with Bob's public key and broadcasts it to everybody. All of Alice's friends will use their own private keys to decrypt the message, but only Bob will ...


Only top voted, non community-wiki answers of a minimum length are eligible