[iter_tool]

Hello everybody
the reason I visited this forum is because I am math student and very interested in AI and computer programming in overall,so my question to you guys : are mathematicians well accepted at AI jobs these days? I love to read about AI topics often and when I have free time ,try to do something on my own.So what are necessary skills for me as a math engineer to be in this industry?

[ivan.moony]

Hello Iter

Industry? AI industry asks for usual programming skills, with the most exposure on AIML (chatbots), NN (neural network pattern recognition process used in i.e. driverless cars) and their derivatives. General math knowledge is always welcome in any programming industry, including industrial AI attempts.

But if you ask what mathematician skills are required in experimental AI field, you might want to take a look at OpenCog, the most popular opensource AGI attempt. In the core of OpenCog system, there lays a kind of mathematical logic. It is a very complicated system (it is a work in progress), and I think they use "probabilistic logic network" to derive knowledge implicitly contained in provided facts. OpenCog makes use of methods such are deduction, induction or abduction, known from mathematician scientific approach. If you really want to get into it, there is a very friendly OpenCog mailing list in google groups where you can get further answers on technology behind OpenCog. They are very open to newcomers, and I'm sure if you pose any relevant question, you can get a useful answer from someone involved in the project, especially if you want to contribute to the project.

If you wondered what technology lays behind Sophia (the AI project currently being under a public spot light), all I can say is that a leader of the project is one of the most prominent chairmen in OpenCog. I'm not familiar with any further details about Sophia.

I believe that behind Alexa, Google Now, Cortana and Siri AI assistants lays a proprietary system analogous to AMIL system, paired with some www operating backend (to order stuff from the web, to make a schedule in your time table, to get the weather info, and stuff like that)

[ranch vermin]

From a guy that didnt do university calculus->
Its actually not important to be fully mathematically trained,  but i tend to use the stuff i learnt in precalculus highschool alot.   just simple stuff,  if your going from 2d images to 3d depth images theres alot of geometry in it, and it can help if your good at algebra.    doing it from a highly trained mathematics standpoint is a different way to look at the problem from a less mathematical person.   they go about it 2 different ways.
Im sure it will help, probably is better to be good at maths.   
Also I get away with numerical calculus instead of doing things purely mathematical - because memory systems end up being tables of values, x->y but I bet having true equations behind what you do definitely would help.

[iter_tool]

Thank you guys for your replies,they were very specific and helpful
especially what you mentioned about this thing OpenCog , i read about it a little bit now and this is a kind of things that I am interested in AI.So I would be very thankful if anyone could suggest something similar to this one.

[unreality]

There's been recent AI headline news about an algorithm that's helping to simulate the brain.

OpenCog as far as I know is not neural networking (A+ IMO). It's also open source, or at least that's what wikipedia says.

[ivan.moony]

I believe OpenCog is currently in a process of choosing some neural network mechanism. I don't know how far did they go by now.

You might want to investigate some of dr. Ben Göertzel's books (the OpenCog-Sophia chairman). Honestly, I didn't read any of his books, but the guy is smart and he shouldn't be joking when it comes to building an AGI system.

Here are some quick Wiki links I thought of this moment, to introduce experimental AI side used in systems like OpenCog (I'm sure there are more systems like OpenCog out there, being open sourced or proprietary):

propositional logic
first order logic
higher order logic
probabilistic logic network
intuitionistic logic

(typed) lambda calculus
intuitionistic type theory
calculus of constructions
lambda cube

(important - necessary to take a short look) Curry-Howard correspondence

Find further details on a materia you find interesting in PDF papers scattered over web. Also you might want to check out automated and semi-automated proof assistants (like Agda, Coq, or HOL) if you believe it might be relevant to your research.

I laid my bets on a kind of typed lambda calculus I'm developing, hoping everything else (including theorem proving) could be described by it.

Let us know if you encounter any interesting project out there

[ranch vermin]

Open Cog is an integration of different methods, its covered alot of ground,  I agree hes pretty good at what hes doing, and hes not just a speculator, he implements as well.

[iter_tool]

Thanks so much guys,this helps me a lot,some of these things you wrote including logic and statistics applied in this kind of projects is what is really exciting for me.I would definitely want to do on projects like this you've mentioned,even something "small" just for myself first.Just keep on with informations ,finally found real answers.

[iter_tool]

This proof assistant softwares...anyone ever got experience with something like this?? Using for private stuff or at work maybe?Does only math professors use them or engineers overall?

[8pla.net]

Mathematical notation comes in handy, I think, to show someone your Artificial Intelligence mathematical equations and formulas without showing your computer programming source code.

[infurl]

This proof assistant softwares...anyone ever got experience with something like this?? Using for private stuff or at work maybe?Does only math professors use them or engineers overall?

You should take a look at AIXI and the work of Marcus Hutter. This page is a good place to start.

http://www.hutter1.net/ai/

In essence, AIXI is an algorithm for artificial general intelligence which is supported by rigorous mathematical proof. It's the real thing, but it can't be implemented yet because it relies on having unlimited processing power. The algorithms like so many other interesting problems are intractable. The challenge is to find a way to approximate them using heuristics.

If you're interest is mathematical theorem proving then take a look at Thousands of Problems for Theorem Provers.

http://www.cs.miami.edu/~tptp/

The topics to learn about here are first order logic and logical resolution. Higher order logic is also interesting but more challenging.

You could also look at ontologies such as SUMO which is open source, and Cyc which is probably the most powerful AI that currently exists. We don't really know how powerful Cyc is because although it has been in development for many decades, it is mostly a secret project.

http://www.adampease.org/OP/

http://www.cyc.com/

Don't forget Mathematica Online. It's some of the smartest software around.

https://www.wolfram.com/mathematica/online/

[iter_tool]

Great,nice things to start,definitely interested in this area(logic,automated theorem proving) since I started exploring AI field.How to start?Reading books about this is the first step of course,but it seems too "heavy" for single person projects??Did anyone ever was included in this kind of projects?

[infurl]

Great,nice things to start,definitely interested in this area(logic,automated theorem proving) since I started exploring AI field.How to start?Reading books about this is the first step of course,but it seems too "heavy" for single person projects??Did anyone ever was included in this kind of projects?

There's no low hanging fruit I'm afraid. You should be prepared to spend decades just getting up to speed.

[ivan.moony]

There is also some web project TPTS (thousand-problems-thousand-solutions) used to test proof assistants. Check also SAT solvers - another, combinatorial kind of proving theorems...

This proof assistant softwares...anyone ever got experience with something like this?? Using for private stuff or at work maybe?Does only math professors use them or engineers overall?

I can imagine scientists using theorem provers in their research. Software engineers also found some use: to prove if their algorithms are behaving correct in any reachable state. This is very important in industries such are airplane controlling software, and I wouldn't be surprised if it was used in automobile industry, knowing that now processors control everything, from responding to brake pedal to fuel injection in motor cylinders. Proving an algorithm correctness could be very profitable task, I've seen multiple big companies invest some hundreds of thousands dollars in projects like those.

In my work, I used online SAT solvers for checking some of my theories (when I was trying to describe higher order logic by propositional calculus constructs), and skimmed over a few real theorem provers. I didn't really used them for anything sane, but I think theorem provers are slightly divided by a fact that none of them can do everything that the other ones do. I guess it has something to do with Gödel incompleteness theorem which states that there is no such system that is complete and correct in the same time. If you want a correct system, you have to give up the completeness. One of math consequences are that you can construct formulas that are correct, but not provable in math. Gödel has also shown a way to construct such a formulas, so it has to be somewhere on the web. Also, I've seen some attempt to disprove this Gödel's theorem, but I'm not smart enough to decide if it was successful. Sorry, I can't find that attempt now, but I know it was at Lambda The Ultimate wall.

There also used to be a public benchmark of success of theorem provers, based on TPTS library, I think. If you want to try some prover, there are online versions which do not require installation (they have web interface), but the most popular ones are needed to be downloaded. By the way, a little bird told me that dr. Ben's current favorite toy tool is "Agda". I think Agda is also a complete functional paradigm programming language. Maybe it would be a good idea to start with that language, and see where the documentation takes you.

[iter_tool]

Thanks a lot,now I have something to start a little bit,this things are very interesting for me, cause this is "intersection" of everything...math,computer science ,AI...one package.