Comment by peter_d_sherman

>" “Ablation studies”: taking an already proved theorem and seeing whether it can still be proved after

removing some key theories or inputs

(e.g., finding an elementary proof for a result currently only provable by non-elementary means)."

As usual, Tao is brilliant in all that he researches, all that he writes about.

I chose the above statement (which is brilliant, in and of itself!) to comment on, because it leads to the following idea:

There there exists, or should exist, a dependency map in the fields of not only Mathematics, but also of Computer Programs/Software, Engineering, and even a seemingly non-related field: The Law...

In other words, how do we get from the simplest of axioms or foundational things (aka "first principles", aka "self-evident truths") to much more complex entities?

In Law for example, how do we go from the simplest of historical legal constructs to the most complex of the most complex Supreme Court cases?

You see, there is, or should be a map, you could call it a dependency map, you could call it a dependency graph, which shows more and more abstract/complex mechanisms/things/assertions/statements/truths/functions which is mapped back to , that is, dependent on various chains, various stackings, various "stacks" of simpler ones.

In Engineering, for example, how do we get from the simplest of machines to the most complex of machines? What simpler machines and/or sub-components (aka "dependencies", aka "subcomponents") are required to build it, and how do those simpler machines work, and what's the dependency graph or map for their subcomponents?

More generalized, if we have something of complexity, then how do we get there, step by step, from individual subcomponents, individual inputs, individual proofs, individual software systems, step by step?

What is the map of those dependencies?

Note that in some systems, Math proofs, for example, there may be different paths which can be traversed to get to the same destination.

Ablation Studies could be thought of in Travel, in Geography as "if I cannot take one, or a specific set of routes to get to a place, can I still get there?"

A simple example would be in Google Maps, where you'd like to drive somewhere, but you'd like to avoid tolls. Is the route still traversable while avoiding tolls? Well, that's an example of one constraint. In Ablation Studies, you might wish to remove a bunch of routes with whatever criteria or characteristics , i.e. muddy roads, roads that have characteristic X, roads that do not have characteristic Y, etc., etc.

Getting back to Math, specifically proofs, it would be great to create a dependency map/graph of all of them, and then try removing inputs (aka, paths to them, dependencies on other mathematical proofs/objects that they may have) and see if they are still reachable.

In software, when we desire the tightest, cleanest, source code, the above is related to refactoring.

In the future, I'd love to see dependency maps/graphs (call them whatever you will) for not just Mathematical Proofs (although I'd love to see that too!), but also in such diverse subjects as Science, Engineering, Programming/CS, and even the Law!

Because they should exist in all of those subjects!

Anyway, another great piece of work by Terrence Tao!