Prove simple theorems in Haskell in automated way I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:
and [n*(n+1)/2 == sum [0..n] | n &lt;- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems involving integers in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.
There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.
Look at Agda [1][2]
I think that it's exactly what you are looking for.
I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html
A very good introduction is plfa [3], also [2]/tutorial-list.html
[1] https://en.wikipedia.org/wiki/Agda_(programming_language)
[2] https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html
[3] https://plfa.github.io/