首页    期刊浏览 2024年11月28日 星期四
登录注册

文章基本信息

  • 标题:A String of Pearls: Proofs of Fermat's Little Theorem
  • 本地全文:下载
  • 作者:Hing Lun Chan ; Michael Norrish
  • 期刊名称:Journal of Formalized Reasoning
  • 印刷版ISSN:1972-5787
  • 出版年度:2013
  • 卷号:6
  • 期号:1
  • 页码:63-87
  • DOI:10.6092/issn.1972-5787/3728
  • 语种:English
  • 出版社:Alma Mater Studiorum - University of Bologna
  • 摘要:We discuss mechanised proofs of Fermat's Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial ``necklace'' proof that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for some of the direct number-theoretic approaches.
  • 关键词:number theory;automated reasoning
国家哲学社会科学文献中心版权所有