Alex,

Before you make any proposals about methods of formalizing anything, please study the work that the international organizations have been doing for many years. I worked with some of those organizations as a representative of IBM (30 years ago), and later when I was working with some start-up companies.

They have some very good people working on those standards, and the specifications they produce are actually IMPLEMENTED in working systems. They are much more than email notes, which people delete after a few days.

Alex: whether it will be a language from the DOL family or Python is the choice of enthusiasts.

No. Emtjusiasts are amateurs. Some of them may be very intelligent amateurs, but anything they do vanishes when they get bored with it. DOL is an professional standard by the Object Management Group (OMG), and it supports other standards by International Standards Organisation (ISO), and the Semantic Web. Those organizations develop standards that are adopted and implemented by professionals for software that is used by thousands or even millions or billions of people.

Following is a reference from my previous note. I urge you to follow the links to the work by PROFESSIONALS in slides 8 to 11 of https://jfsowa.com/talks/eswc.pdf

John

From: "Alex Shkotin" <alex.shkotin@gmail.com>

JFS:"To Alex: There is no need for you (or anybody else) to lean Python. With the DOL standard, any syntax that conforms to the ISO standard for Common Logic can be automatically translated to and from any syntax that can express FOL or many subsets and supersets of FOL. That includes OWL, Turtle, UML, and even TPTP (Thousands of Problems for Theorem Provers)."

The situation is just the opposite. Formalization of a unit of knowledge (in this case, two theorems) can be placed in the framework of the theory (exactly this one!) in any language. The main thing is that there are enthusiasts who undertake to formalize this particular theory in this particular formal language. And whether it will be a language from the DOL family or Python is the choice of enthusiasts.

The beauty of formalizing a unit of knowledge is that they are usually small (definitions can be several sentences long), of course, except for proofs that can take up terabytes (but in this case it's initially formal). The main thing is that the new unit is consistent with those already in the framework. This structure of the framework of the theory is known but not simple........