论文给出了Ramsey定理自动证明的代数化方法，并使用符号计算软件实现了R(3,3)=6 和R(3,4)=9 的自动证明, 并讨论了处理更复杂情况, 包括R(3,5)=14 和R(3,3,3)=17 等情形的分治法. 不同于以往的计算机辅助计算方法，本文通过将Ramsey问题转化为有限域上的多项式的展开合并过程，得到了Ramsey定理的机械化证明. （论文申请投稿《系统科学与数学》）