N.A. Shanin was born on 25 May 1919 in Pskov where his father was a physician. In 1935 Shanin enrolled in the faculty of Mathematics and Mechanics of the Leningrad State University and in 1939 he became a graduate student. His supervisor was A.A. Markov whose ideas and personality had a formative influence on Shanin's scientific interests. In 1942 he defended his Ph. D. dissertation "Extensions of topological spaces" and in 1946 his D.Sc. dissertation. From 1941-1945 Shanin served in the Red Army. In October 1945 he became a Research Fellow at the Steklov Mathematical Institute (Leningrad Branch) of the Russian Academy of Sciences where he is still working. In addition to his work at the Mathematical Institute, Shanin is also a Professor of the St.Petersburg University.


N.A. Shanin (on the left) and A.A. Markov

In 1940-ies he worked in topology, but later, under Markov's influence he became one of founders of Russian constructivist school in mathematics. In 1950-ies Shanin constructed a series of embedding operations from classical arithmetic into intuitionistic arithmetic preserving some theorems containing existence and disjunction. Previous (negative) translations "killed" these constructive connectives. This was one of the first publications in the USSR on constructive mathematical logic and had a considerable influence on the development of research in this field. Soon after that Shanin published a modification of Kleene's realizability interpretation which formed a basis of formulation of semantics in Russian constructivist school. He outlined and (together with other researchers) carried through a program of developing constructive functional analysis base on the notion of completion of a metric space. This was a starting point of numerous investigations in the USSR, Czechoslovakia, Hungary, France and Egypt.

In 1961 Shanin organized a group of mathematical logic at the Leningrad Branch of the Mathematical Institute. The group created the first computer program of producing natural deductions which would be as close as possible to a form easily perceived by a human. Ideas proposed by Shanin stimulated further progress in automated deduction and proof theory in general. Leningrad School of Proof Theory got international recognition.

Developing constructive semantics, N. Shanin proposed majorization approach when compound statements are approximated by quantifier-free formulas.