Closed xamidi closed 2 years ago
Hi, thanks for noticing my project. The project is not in a final state. But actual project repository is not this one (dmitry-vlasov/russell) but rather this one: https://github.com/dmitry-vlasov/russell-flow There I completely rewrote the project in another language - flow9. The reason - writing in flow9 is x10 more efficient then using c++. Current state of the project: formal math language is developed, translation forth/back to Metamath works, some interesting features like automated proof optimizations (shortening) works, another interesting feature: automatic generalization of a theorem statement by generalizing a proof also works.
Nice interface in vscode editor with instant intellisence-like highlighting of mathematical stuff and navigation throughout the theorem base also works.
About automated proving: in current state such facility is implemented as a general algorithm of proof search, but obviously it's not efficient since it's quite straightforward thus not smart. I'm going to research this topic in the direction of implemented machine learning on the basis of a hand-written proofs as dataset, so that algorithm becomes much smarter.
Currently I'm reworking flow9 compiler - trying to build a new c++ backend which should be more memory efficient then java-based one, used currently. In the current state the complete translation of Metamath theorem base set.mm demands 7Gb of memory to complete, I want to decrease it at least two times.
So, concluding the above, I'm still developing my formal math system and find it potentially very powerful and attractive. If you want to test it - feel free to download it, compile, run and explore the Metamath theorem base in Russell format. In case of any problems/questions feel free to contact me. My telegram id: https://t.me/vlasov_dmitry
Look of Russell code in vscode with the Russell extension installed
Very nice. Currently I am not in need of such a tool but likely I will be in the future. Thank you for your great work.
I noticed there hasn't been a commit in almost 3 years but you are active on other projects, so I wonder..
mdl will support fully automatic proving facility
simply take a while? Or is that already in a state you are satisfied with?