Nikolai Shanin

[1] His father, Alexander Protasyevich Shanin (Russian: Александр Протасьевич Шанин, 1886–1973[2]), 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.

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),[3] where he worked until the end of his life.

[6] 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.

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.

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.

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.

The group's initial goal was to develop and implement an algorithm for automatic theorem proving, focusing primarily on classical propositional calculus.

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).