Implement basic linear algebra in Idris (checking with proofs for linear dependence, finding eigenvalues and eigenvectors with proof, diagonalizing matrices, etc).
I think this project is sufficiently mathematical to be interesting and also does not require too many definitions to get started on.
It is certainly a good project. Linear equations is the first step for this. It will take work though, since eigenvalues will need reals, or at least algebraic numbers, which is a project in itself.
I suggest the following project:
Implement basic linear algebra in Idris (checking with proofs for linear dependence, finding eigenvalues and eigenvectors with proof, diagonalizing matrices, etc).
I think this project is sufficiently mathematical to be interesting and also does not require too many definitions to get started on.
Would this be a good idea?
--Abishek