# Status of declarative proof languages in proof assistants

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!

• You may want to look at the standard proof library of TLAPS, the (quite beautiful) declarative proof language for TLA+: github.com/tlaplus/v2-tlapm/tree/master/library (the files ending with _proofs.tla). TLAPS is deeply integrated (it's the only proof language for TLA+) and actively maintained. – pron Dec 14 '16 at 8:38
• Czar is not very popular in the Coq community and not actively maintained anymore, but Isar langage is widely used in Isabelle/HOL formalizations. I am not aware of any other mature system supporting declarative proofs. – Julien Narboux May 11 '17 at 7:44