Nikolai Shanin

Nikolai Aleksandrovich Shanin (Russian: Николай Александрович Шанин) was a Soviet and Russian mathematician and the founder of a school of constructive mathematics in Leningrad (now Saint Petersburg). He was born on May 25, 1919, in Pskov, Russia, to a family of doctors and passed away on September 17, 2011, in Saint Petersburg, Russia. His father, Alexander Protasyevich Shanin (Russian: Александр Протасьевич Шанин, 1886–1973), was a well-known specialist in skin cancer.

In 1935, N. A. Shanin entered the Faculty of Mathematics and Mechanics at Leningrad State University and began his PhD studies there in 1939. Andrey Andreyevich Markov, Jr. became his supervisor, while his second supervisor was Pavel Sergeyevich Alexandrov. Markov’s ideas and personality had a decisive influence on the development of Shanin’s research interests.

In 1942, he defended his PhD dissertation, “On the Extension of Topological Spaces,” and in 1946, his D.Sc. dissertation, “On the Product of Topological Spaces.” From 1941 to 1945, during the war between the USSR and Germany, Shanin served in the Red Army. In October 1945, he became a senior research fellow at the Steklov Mathematical Institute of the USSR Academy of Sciences in the Leningrad (later Saint Petersburg) division (LOMI/POMI), where he worked until the end of his life.

While working at the Academy of Sciences, he also taught for many years at Leningrad (later Saint Petersburg) State University in the Faculty of Mathematics and Mechanics—where he became a professor in 1957—as well as in the Faculty of Philosophy.

Shanin’s research activity can be divided into two periods: topological and logical-constructivist. The first period lasted until the late 1940s. His contributions to general topology remained influential for many years.

The second period, which lasted much longer, not only produced numerous scientific results but also led to the formation of a major Leningrad school of mathematical logic and proof theory. This work extended into areas such as computability (e.g., Yuri Matiyasevich), algorithmics, computational complexity, and the application of computers to mathematical research.

For A. A. Markov Jr. and later N. A. Shanin, the ineffectiveness of purely existential theorems was a source of "discomfort" in the foundations of mathematics, making the ideas of intuitionism particularly appealing.

N. A. Shanin began by generalizing the approach of A. N. Kolmogorov and K. Gödel on embedding operations that transform a formula F of classical logic into a formula Fᶜ' of intuitionistic (constructive) logic, such that Fᶜ' is deducible in intuitionistic logic if and only if F is deducible in classical logic. Moreover, this transformation aimed to preserve the syntax of F as much as possible.

Shanin developed a series of sophisticated and general operations and, in particular, described classes of classical formulas containing ∃ and ∨ that remain deducible in intuitionistic logic without modification. This paper was among the first works on intuitionistic logic (a term often replaced by "constructive" logic, in part for political reasons) in the USSR and significantly influenced research in the field. Later, Shanin applied his ideas to other formal systems.

N. A. Shanin’s next area of research focused on constructive semantics and was also influenced by intuitionism. However, the semantics of intuitionism was somewhat vague. The first rigorous semantics for intuitionistic logic was S. C. Kleene’s realizability. According to Kleene, a formula ∀x∃y A(x,y) is true if there exists an algorithm that, for each x, constructs y such that A(x,y) holds. In Kleene’s realizability, however, the transformed formula is not necessarily simpler than the original one.

Shanin introduced a procedure (algorithm) known as the **elicitation of constructive problems**, which reduces the initial formula to a formula of the form ∃x₁...∃x_kF , where F contains neither ∃ nor ∨. Due to embedding operations, it then suffices to prove F within classical logic. This procedure significantly facilitated communication between the Russian constructivist school and constructivists in the West, particularly intuitionists.

Kleene later observed that, in purely logical terms, Shanin’s algorithm follows from just two principles: Markov's principle and a variant of the Church–Turing thesis. Further development of these ideas led to a **finitary** approach (in the sense of Hilbert) to constructive mathematics.

Building on constructive semantics, N. A. Shanin began, in the mid-1950s, a revision of classical mathematics—particularly calculus and functional analysis—from a constructivist perspective.

A priori, it is not obvious which notion of a computable real number is the most productive. Shanin defined a **constructive real number** as a "duplex," where both rational approximations and the rate of convergence are given by algorithms, and demonstrated that this approach is effective. Similar algorithmic approaches to real numbers were later developed in the West (see computable number).

In 1961, N. A. Shanin organized a **mathematical logic** research group at the Leningrad Department of the Steklov Mathematical Institute of the USSR Academy of Sciences. The group's initial goal was to develop and implement an algorithm for automatic theorem proving, focusing primarily on classical propositional calculus.

The first three members of the group were Gennady Davydov (1939–2016), Sergey Maslov (1939–1982), and Grigory Mints (1939–2014). More researchers joined in subsequent years, including V. P. Orevkov [1], A. O. Slissenko, and Yu. V. Matiyasevich.

During this period, there was widespread global enthusiasm for automatic theorem proving, particularly in pure logic. Starting from Gentzen’s sequent calculus, Shanin developed a proof search algorithm designed to produce **natural, human-friendly proofs**. He emphasized the use of heuristics and aimed to generate results in the form of **natural deduction**.

The algorithm was successfully implemented and demonstrated excellent performance.

N. A. Shanin was a dynamic and energetic professor who excelled at explaining fundamental concepts of logic, particularly those lacking formal mathematical definitions, using simpler notions (e.g., integers). His analysis of various semantic issues had a significant influence on philosophers.

• Vsemirnov, M A (2001), "Nikolai Aleksandrovich Shanin (on his 80th birthday)", Russian Math. Surveys, 56 (3): 601–605, Bibcode:2001RuMaS..56..601V, doi:10.1070/RM2001v056n03ABEH000412
• Vsemirnov, M A; et al. (2013), "Nikolai Aleksandrovich Shanin (obituary)", Russ. Math. Surv., 68 (4): 763–767, Bibcode:2013RuMaS..68..763V, doi:10.1070/RM2013v068n04ABEH004852

• Nikolai Shanin at the Mathematics Genealogy Project
• Nikolai Aleksandrovich Shanin at the Steklov Institute of Mathematics at St. Petersburg