> But nothing major, that will somehow massively reduce the complexity of understanding mathematics by non-experts.

To give just one example, when done properly the use of hinting in the multi-line equational proof format will certainly ease the non-expert’s task of following a proof.

The two-column proof has been a thing in math education for over a century [1]. I have been told by math educators that it is almost universally detested by school students, because of how it restricts their thinking. Nevertheless, it would be useful at the research level to include more of this hinting. But hinting is not a notational issue at all.

[1] https://deepblue.lib.umich.edu/bitstream/handle/2027.42/4265...

The equational and two column proof formats aren’t the same. Perhaps you should read Dijkstra’s monograph’s section on it to understand the differences. And to say they are somehow isomorphic is to miss the point entirely. Sure “x is equal to y” means the same as “x = y”, but even the traditionalists recognize the merits of Recorde’s notational device, even if they fail to follow the greater implications thereof.