Theoretical computer science is an area of mathematics that studies problems that we can — and that we cannot — compute, transmit, reach an agreement over a communication channel. It originated from the mathematical logic and the foundations of mathematics after the seminal works of Kurt Gödel in proof theory, Claude Shannon in information theory, and Alan Turing in theory of computation.
The computational complexity theory deals with classes of computational problems rather than with specific problems. A class consists of problems that can be solved in a certain computational model with a certain amount of resources (running time, memory, communication, etc.). The P versus NP question (one of the `millenium problems’) is one of the open questions in this theory that received publicity far beyond mathematicians: is there a polynomial-time algorithm that can check that a Boolean formula is a contradiction? While many natural questions in this area are still open, there are also marvellous and unexpected theorems (IP=PSPACE, MIP=NEXP, PCP-theorem, etc.). One of the most rigid models for studying the complexity, Boolean circuits, which make the theoretical model of digital electronic circuits, measures the complexity in terms of the number of elementary operations.
Does every theorem have a short proof? This question remains open even in the `easiest’ case of propositional proofs (where we have only Boolean variables and binary connectives such as and, or, not), where it is equivalent to the NP vs coNP question of the computational complexity theory. While the questions remains open in general, exponential lower bounds are known for speficic proof systems. Cook’s program in the propositional proof complexity asks for proving exponential lower bounds for more and more powerful proof systems, which requires newer and newer concepts and methods that range through all the mathematics (algebra, geometry, combinatorics).
Among the people working in this field are Edward A. Hirsch and Dmitry M. Itsykson.
A lot of problems emerging in applications (for example, scheduling, transportation problems, program verification, circuit verification) are NP-hard, which means in particular that noone is able to solve them in a reasonable amount of time in the worst case. In theory. However, we need to solve them anyway. Some of the approaches here are `weakly exponential’ algorithms, parameterized algorithms, approximation algorithms.
Computational geometry is a field in theoretical computer science, which borders discrete geometry. Computational geometry deals with various problems corresponding to computations with discrete geometric objects. Its main goal is creating efficient and provably correct algorithms for such problems, and also analysing their complexity, in particular, proving NP-completeness for some of them. Often, but not always, the problems have direct practical applications. Often, in order to create an efficient algorithm, one first needs to investigate the properties of corresponding geometric objects, which is a separate problem in discrete geometry.
Discrete mathematics, or combinatorics, deals with the most simple structures: finite sets, the families of their subsets (like graphs), finite words, finite systems of integers and so on. For answering the important and natural questions about such matter both elementary properly combinatorial methods and advanced theories dealing with richer structures (algebra, probability theory, topology, ergodic theory, etc.) are used. The great mathematician of XX century I.M. Gelfand used to say that the combinatorics will become the central part of the future mathematics. The mutual impact of discrete and continuous mathematics is now so total and important that this prediction may be called confirmed.
One of the main aims of mathematical logic is to develop and study formal models of different sorts of language phenomena — from semantical and grammatical problems arising in natural languages to deductive and algorithmic properties of mathematical theories and semantics of programming languages. In particular, among the achievements of mathematical logic are formalisations of the notions of a proof and of a computable function, and also classical results on deductive underivability (e.g., of the continuum hypothesis within axiomatic set theory) and algorithmic undecidability (say, of elementary group theory). Logical methods allow us to describe, with enough accuracy, syntax and semantics of various languages, and then study them successfully as mathematical objects. Mathematical logic is concerned with both the deductive/algorithmic function of languages and their descriptive function. It has a wide range of applications, including, among others, computer science, linguistics, and formal philosophy. It is intimately connected with the foundations of mathematics and computer science. Among the key logical notions are `provability’, `computability’, `expressibility’ and `truth’.
Stanislav O. Speranski is working in this area.