In the essay, the importance of dependency on previous concepts is touched upon multiple times.
I essentially see 2 distinct "problems" or tasks that would need to be done in this specific respect (without downplaying the value of other factors): 1) it takes effort to encode the dependency relationships, 2) even if someone puts in a lot of work for a specific subject or domain to encode the dependency relationships, we need to modify the tools to take advantage of this knowledge.
I would propose as a next testbed, one takes the MetaMath database (set.mm), since dependency of a theorem on other theorems or axioms can be extracted in automated fashion. So I would love to see a tool (a working title could be Anki/MetaDrill or "autodidact" was the title I had in mind) that presents me with the following exercises:
type 0a, 0b: given ascii characters select LaTeX symbol (a) and vice versa (b) [for example ".-" for negation etc...]
type 1: given theorem/hypothesis/axiom/definition abbreviation name: produce the statement
type 2: given theorem/hypothesis/axiom/definition statement: produce the abbreviation (the reverse of exercise type 1, both can be easily extracted from an instance of a verifier that has parsed the set.mm database)
type 3: given a couple of input statement, and an output statement: produce the theorem abreviation that justifies this step (can be easily done by randomly selecting a target theorem from those scheduled for the user to know, then searching all proofs in the database for steps that reference the target theorem, each reference to the theorem is a utilization or example application of the theorem)
type 4: given a theorem: produce the list of theorems directly used in its proof (this one depends on the proof used, so that it is possible to find proofs that don't rely on those in the database, but is easy to generate for the proofs proposed in the database: just enumerate all the references in the proof of this theorem)
type 5: given a theorem (by abbreviation or by statement): produce a proof (the previous series of exercises should provide all the prerequisites, and the last exercise above would contain a lot of hints to reproduce the proof) it is possible to find an original proof, and the MetaMath verifier can be used to check the user's proof!
the exploration or presentation of new axioms, definitions, theorems, can be limited to those "in view" to the user, using the dependency graph of theorems, so only a minimal number of new concepts is introduced at a time. I.e. this prevents the user from being bombarded with uncontextualized facts like "the connected sum of a torus with a sphere is a torus" without first learning about addition of rational numbers...
once a large number of people can quickly get up to speed with MetaMath, they will see the utility of spaced repitition, and understand that formalization is the way forward, since formalization automatically forces you to be explicit in dependencies, and forces people to state their beliefs as exactly as possible, or alternatively as quickly as possible (be bold), but such that others can prove errors in their conjectures by providing proof that the bold person happened to introduce an inconsistency.
But the biggest advantage of logical formalization of knowledge is that all the above exercises can be automatically generated, no one needs to produce flash cards! not only can they be generated automatically, they can be generated as a function of the past performance of the user on those exercises, instead of waiting a long period of time before retesting prerequisites 2 or 3 levels deep, we can test already seen knowledge that relies on it, and upon failure schedule the immediate prerequisites it relies on 1 level deeper, most of which will succeed, but one of which will typically fail again prompting it's lower level prerequisites to be tested (2 levels deeper from the original failure) to finally prompt a last failure, upon which the 3rd level lower prerequisites are reached but all succeed, just like how a professor in an oral exam probes where exactly the student got stuck. This allows to test for gaps in working memory to be detected without explicitly testing all the lower levels, just like the blood test during the second world war: at some point an expensive but very sensitive test was developed, and instead of testing the soldiers individually, their blood was mixed then tested, and in this manner it was possible to cheaply scan for positives and only zoom in when a group had a positive. I can not find the link to the relevant wikipedia page sadly.