Prove-It
Prove-It copied to clipboard
sandialabs
A tool for proving and organizing general theorems using Python.
Need to check 'is_applicable' for known_memberships in linear_algebra and quantum algebra packages
InClass.yield_known_memberships does this properly where it checks 'is_applicable'. However, this doesn't appear done properly for yield_known_hilbert_spaces in the linear_algebra package or when using MatrixSpace.known_memberships in qmult.py. This can cause funny...
I'm not sure how well this would work or if it would be desirable, but what if n-ary functions were implemented as definitions outside of the core? This would simplify...
Make enhancements and fixes to the quantum algebra package, including the following as a first batch of updates: 1. Fix the bra_def axiom and KEEP the qmult_of_bra_as_map theorem. qmult_of_bra_as_map has...
When "literal generalization" derivation steps are made, they depend on the dependencies of used theorems. This requires theorem proofs to be executed in a specific order, unlike any other derivation...
It's not clear how consistently this error arises, but over the past few months we have seen 404 not found error when initially trying to access the proof notebook for...
In working on database-related stuff in the TheoryFolder and TheoryFolderStorage classes, we discovered an inconsistency in the use of object hash_ids in the name_to_hash.txt files and in the subsequent processing...
It can be very confusing when two expressions look the same but are actually different. Here are two things we can do to avoid this problem. 1. When checking to...
The broader development/enhancement issue, of course, is the implementation of an independent general proof checker within the Prove-It system that would deal with all possible types of proof steps and...
Prove-It currently fails in the following example (a simplified version of something we encountered during a meeting to help Jamie prove proveit.number.sets.integer.successiveNats, if I remember correctly): In [1]: from proveit._common_...
Metadata
Owner
Metadata
A tool for proving and organizing general theorems using Python.