The Coq mailing list

[Rustam Zhumagambetov <rustam.zhumagambetov AT nu.edu.kz>]

Dear all,

I want to present a new solution for running Coq on Android devices - Coq Telegram bot. 

It allows you to continue working on proofs even on the go. 

Link to the bot: http://t.me/CoqProofbot

This is part of an undergraduate research project.

The only data we collect - number of unique users.

After using the bot, we kindly ask you to take the survey to gather feedback and identify the need of such bot for the community. As this is public beta we want to attract attention from the community, gathering your feedback on what features bot should possess. Currently we also have single user bot that can be run from any machine that have Coq and Java in it. 

Link to the survey: https://goo.gl/forms/E3cEDvnM7KFYB4AP2

Here is an example of proving a simple theorem:

It also supports loading of external files, just drop them into the bot (.v files).

Screenshot: https://image.ibb.co/kuVecm/chat_screenshot.png

Kind regards,

Rustam Zhumagambetov