Tristan: Incremental Linear Algebra or Incremental Theorem Proving
I have two project ideas:
Incremental linear algebra. Many problems in the area of Social Network Analysis and “Big Data” can be expressed in the language of linear algebra. A library for incremental sparse linear algebra would allow for faster computations on changing real world graphs. I would like to create a proof of concept by starting with sparse matrix - dense vector multiplication. My first goal is to characterize the typical changes a real world graph would experience over time. This will guide my implementation.
Incremental theorem proving. There has already been some research into this topic. Often theorem proving is done in an interactive manner. Supporting incremental proving is essential for user interaction. I believe existing systems do not support sharing sub terms between different proof. Adding support for this could speed up computation time. I will need to verify that enough shared subterms regularly exist for this to be worthwhile.