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.