Visualize the dependency of mathematical theorems and proofs. A blend of the Bourbaki tradition, formal proof system, reverse mathematics, and readable prose.
Public
Edited
Mar 23, 2023
Importers
1 star
function Prop(name, statement, proof=[], replace={}, reserved=[]){
this.name = (s=name)=>s
this.reserved = reserved
this.hidden = (s)=>s
if (!Array.isArray(statement))
statement = [statement]
let keys = Object.keys(replace)
for (const key of keys) {
statement = statement.map(x=>x.replace(key, replace.key))
}
this.statement = statement.map(x=>greyblock(x))
if (!Array.isArray(proof))
proof = [proof]
this.proof = proof
}
function Proposition(name, statement, proof=[], label=null){
this.name = (s=name)=>s
this.label = (label == null) ? name.replace("_", " ") : label
this.hidden = (s)=>s
if (Array.isArray(statement))
this.statement = statement.map(x=>greyblock(x))
else
this.statement = greyblock(statement)
// if (!Array.isArray(proof))
// proof = [proof]
this.proof = proof //.map(x=>md`x + '<div style="text-align: right"> ${tex`\square`} </div>'`)
}
function Definition(name, definition, proof=[], label=null){
this.name = (s=name)=>s
this.label = (label == null) ? "def: " + name.replace("_", " ") : label
this.hidden = (s)=>s
this.definition = definition
}
greyblock = (x)=> md`<div style="background-color:#eeeeee; width:${Math.min(640, width)}px">${x}</div>`
greymargin = (s)=>md`<blockquote style="border-left:5px solid #eeeeee">${s}`
graph = dot`digraph "${id}" {
rankdir = ${orientation};
Taylor [label="Taylor's Theorem"]
least_upper_bound [label="least upper bound\nproperty"]
real_numbers [label="def: real number" shape=box]
continuous [label="def: continuous" shape=box]
differentiable [label="def: differentiable" shape=box]
integral [label="def: integral" shape=box]
properties_of_integral [label="properties of\nthe integral"]
const_fn [label="constant function"]
FTC -> "Taylor"
"properties_of_integral" -> "Taylor"
"properties_of_integral" -> "FTC"
"FTC1" -> "FTC"
"const_fn" -> "FTC"
"differentiable" -> "FTC1"
"properties_of_integral" -> "FTC1"
"continuous" -> "FTC1"
"integral" -> "properties_of_integral"
"continuous" -> "properties_of_integral"
"least_upper_bound" -> "properties_of_integral"
"real_numbers" -> "integral"
"real_numbers" -> "continuous"
"real_numbers" -> "least_upper_bound"
"MVT" -> "const_fn"
"real_numbers" -> "differentiable"
"continuous" -> "differentiable"
"EVT" -> "MVT"
"differentiable" -> "MVT"
"continuous" -> "EVT"
"least_upper_bound" -> "EVT"
}`
edges = Array.prototype.concat.apply([], [0,1,2,4].map(i => module.default.modules[i].variables))
.filter(v => !v.from) // Don’t graph dependencies of imports.
.filter(v => v.name)
.filter(v => v.inputs.includes("Proposition") || v.inputs.includes("Definition"))
.map((v, i) => {
const inputs = v.inputs.filter(i => !["tex", "md", "width", "greyblock", "width_style", "Proposition", "Definition"].includes(i));
const name = v.name || `#${i}`;
return inputs.map(input => `"${input}" -> "${name}" ${input}`).join("\n")
})
.join("\n")
module.default.modules[0].variables[9]
One platform to build and deploy the best data apps
Experiment and prototype by building visualizations in live JavaScript notebooks. Collaborate with your team and decide which concepts to build out.
Use Observable Framework to build data apps locally. Use data loaders to build in any language or library, including Python, SQL, and R.
Seamlessly deploy to Observable. Test before you ship, use automatic deploy-on-commit, and ensure your projects are always up-to-date.