最近想通过编程来巩固数学，我用的是Julia
我记得以前写过 project euler，而最近我在学微积分，概率论等内容，不知道有没有这种网站技能提高数学，又能提高编程能力
ps: 我为什么查不到几何那些的编程
这位道友啊，我看过你之前的帖子，我记得你好像比我小一届，因此我推测，你学数学应该是在准备考研吧？
如果我的推测没有错的话，那我给你一个忠告，给你热情浇一盆冷水。。。这也是我的教训。不过我下面的话只是一家之言而已，也可以不听。
私以为
编程不是万能的，“什么都可以通过编程来解决”这样的想法不太现实，很有机械唯物主义的味道。学数学就是学数学，一些考研数学问题的求解方法在计算机里面都是比较暴力的，比如极限还有微分，根本对考试学习没有任何帮助（委婉一点说就是帮助不大）。通过编写程序来学习数学只是缘木求鱼，真要学习数学不如多买一叠A4草稿纸，多练习计算。
19 个赞
这个想法奇特，我也想知道
codeforces上带math和几何标签的题目？
认识个整数学的人用 APL 写泰勒展开的的
有兴趣你可以问问他，或者我帮你问也行。
数学编程, 那不就是 mathematica 
1 个赞
打开HoTT book，把里面数学都形式化了
software foundation?
建议读sicp
1 个赞
我曾经沉迷于用Coq，Agda这些Proof Assistant去做数学推导，但大部分时候证明的都是极其琐碎的细节。这些步骤在经典的数学推导中往往就是一句“易验证…”。
且读数学书的时候，或有精妙绝伦的构造，令人看完拍手称妙，亦有数形结合，直观易懂。而看形式化证明的时候就不会，大部分时候只有机械化的操作，并没有太多思维上的深度。（当然也可能是我看得不够多）
这大概也是为什么大部分数学家都不接受形式化证明，因为对数学家来说，数学的“美”是比证明更重要的。一个绝妙的证明思路只能妙手偶得，而一个繁琐机械的证明大概只要雇一个PhD花几年就可以做出来了。
2 个赞
我最近在学ocaml。什么moudle type、functor等语法知识点都已经把人搞晕了。
这不就是函数式语言吗，为什么他们要弄得这么晦涩
module type 约等于 interface， functor 约等于 abstract class
这是连 Java 都没学好才觉得晕。
因为你没用过工业人用有高自动化的 prover，Coq Agda 如果说是手动档的话，自动档有 Isabelle, ACL2，还有无人驾驶的 Eprover，Z3
ACL2 可以自动证明复杂的系统，Eprover 能证出来的东西人类都不一定能看懂。
你说的这些我只用过Z3，但我了解得很粗浅，只是把它当作约束求解器来用，类似于解方程组的功能，跟我理解的数学证明还是有点差距。
当然，在应用领域，形式化验证是很有价值的，可以提供高可信的软硬件系统。私以为PL整个领域也正由理论走向应用，毕竟理论上已经很久没有什么实质的进展了。
不过回到楼主的问题，对于做数学，还是按部就班用草稿纸最实在。
1 个赞
为啥用草稿纸，有CAS做 symbolic computation， solving，plotting 也挺香啊。
实际上有兴趣有能力给开源的 CAS 如 maxima，fricas 提交代码也挺好的，用户里面有很多做数学和统计的。
我做积分作业的时候，fricas 积分的结果形式和用积分技巧的不一样，我就用 fricas 写了个专门用来做作业的积分。当然这个前提是我们考试远比作业简单，都是 set up problem 连计算器都不用，而作业是按用图形计算器的难度出的。
1 个赞
一个简单的比喻而已。比如随便引用一下
A functor is similar to an abstract class with a constructor that consumes an interface and produces a new class.
This isn’t entirely accurate but it was enough to start making my own functors.
https://medium.com/@Pooch/functors-first-class-modules-in-reason-b4bb1461d849
Reason 是一个 OCaml 的语法煻。