Brand new user, and joining the party kind of late, but hoping to get the most out of the rest of October by focusing on this!!!
Project: Moss on Stone (A Theorem Proving Assistant for Obsidian)
Background: I started using Obsidian as a way to take smart notes for pure maths. I’m still iterating and improving on my workflow, but at the moment there are two basic types of notes: definitions, and propositions,. Each have a basic title, a short english description, a formalization, and optional additional descriptions.
So far I have gotten an immense amount of utility by seeing which definitions are linked to which theorems. The next natural step is to add notes which are proofs of the theorems, and devising a digital scratch pad/workflow that facilitates this.
Today I am just writing this post as a way of getting my initial thoughts out there and as a way to commit to this daily progress.
MVP Feature List:
3 panes
- Main pane: has an input for hypotheses and conclusions and this is where we will be left to do symbolic manipulations and scratch work
- Definitions pane: Lists all the definitions inside of the theorem, and all of their logically equivalencies. There should be some way of marking which definition is the main definition
- Related theorems: Shows all of the theorems in your vault which make use of the definitions which you are using. Potential to organize them by hypothesis and conclusions split. Also some type of recommendation system for which theorem would be the most helpful would be totally, totally sick.
Notes:
-At the moment this is particular to my own note taking workflow (which is still in it’s infancy)
-Consulting Polya’s books on induction and discovery could provide good motivation.
-Getting some
-Getting a more concrete specification of which cognitive tasks (ex. memorization…) are involved in theorem proving would greatly improve this project’s scope (As well as make me a better mathematician, which is what this is all about)
Dreaming dreams spit ball list
-Mobile support
-Way out there (Using RegEx or AI in order to formalize written proofs and/or theorems into lean so as to verify that the proofs which we have written are in fact correct and rigorous)