I'm interested in formalising mathematics and logics in a proof assistant, both to get to know a proof assistant and to make an archive of proofs for myself (nothing too fancy, mainly first order logic, set-theory, group-theory and so on).
To be useful as an archive it is important to be able to formulate the proof in a human-readable way which should be possible with the declarative proof languages (e.g. Czar for Coq and Isar for HOL/Isabelle).
But I haven't found a lot of material (especially proof examples) for both languages (Czar,Isar) and literature on the subject stops around 2005. Both languages seem to be somewhat abandoned (the declarative languages, not the proof assistants themselves).
Now my questions are:
- General questions on formalising math/logics:
- Has anybody experience in formalizing math in a declarative way?
- What are the limitations of this approach?
- Are the resulting proofs digestible to the human reader without running the script in parallel (which is necessary e.g. for Coqs' tactics language)?
- Question concerning the integration status in proof assistants:
What is their current status - are they deeply integrated into the systems and actively maintained? Or is this subject abandoned (if so, why)? I can't find any recent material on both Czar and Isar.
- Possible alternatives:
Besides Coq/Czar, Isabelle/Isar and Mizar are there any other mature systems that allow for declarative proofs?
Thank you very much!