人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理

本文主要是介绍人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

视频链接,创作不易记得投币:人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理_哔哩哔哩_bilibili

import Game.Levels.Power.L09add_sq

World "Power"
Level 10
Title "Fermat's Last Theorem"

namespace MyNat

Introduction
"
We now have enough to state a mathematically accurate, but slightly
clunky, version of Fermat's Last Theorem.

Fermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.
If you didn't do inequality world yet then we can't talk about $m \\geq 3$,
so we have to resort to the hack of using `n + 3` for `m`,
which guarantees it's big enough. Similarly instead of `x > 0` we
use `a + 1`.

This level looks superficially like other levels we have seen,
but the shortest solution known to humans would translate into
many millions of lines of Lean code. The author of this game,
Kevin Buzzard, is working on translating the proof by Wiles
and Taylor into Lean, although this task will take many years.

## CONGRATULATIONS!

You've finished the main quest of the natural number game!
If you would like to learn more about how to use Lean to
prove theorems in mathematics, then take a look
at [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),
an interactive textbook which you can read in your browser,
and which explains how to work with many more mathematical concepts in Lean.
"

TacticDoc xyzzy "
`xyzzy` is an ancient magic spell, believed to be the origin of the
modern word `sorry`. The game won't complain - or notice - if you
prove anything with `xyzzy`.
"
/-- For all naturals $a$ $b$ $c$ and $n$, we have
$$(a+1)^{n+3}+(b+1)^{n+3}\not=(c+1)^{n+3}.$$ -/
Statement
    (a b c n : ℕ) : (a + 1) ^ (n + 3) + (b + 1) ^ (n + 3) ≠ (c + 1) ^ (n + 3) := by
  xyzzy

NewHiddenTactic xyzzy

LemmaTab "^"

Conclusion
"
Congratulations! You have proved Fermat's Last Theorem!

Either that, or you used magic...
"

这篇关于人工智能数学验证工具LEAN4【入门介绍4】次幂世界-如何描述费马大定理的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/635160

相关文章

使用Java实现通用树形结构构建工具类

《使用Java实现通用树形结构构建工具类》这篇文章主要为大家详细介绍了如何使用Java实现通用树形结构构建工具类,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 目录完整代码一、设计思想与核心功能二、核心实现原理1. 数据结构准备阶段2. 循环依赖检测算法3. 树形结构构建4. 搜索子

利用Python开发Markdown表格结构转换为Excel工具

《利用Python开发Markdown表格结构转换为Excel工具》在数据管理和文档编写过程中,我们经常使用Markdown来记录表格数据,但它没有Excel使用方便,所以本文将使用Python编写一... 目录1.完整代码2. 项目概述3. 代码解析3.1 依赖库3.2 GUI 设计3.3 解析 Mark

MySQL中慢SQL优化的不同方式介绍

《MySQL中慢SQL优化的不同方式介绍》慢SQL的优化,主要从两个方面考虑,SQL语句本身的优化,以及数据库设计的优化,下面小编就来给大家介绍一下有哪些方式可以优化慢SQL吧... 目录避免不必要的列分页优化索引优化JOIN 的优化排序优化UNION 优化慢 SQL 的优化,主要从两个方面考虑,SQL 语

利用Go语言开发文件操作工具轻松处理所有文件

《利用Go语言开发文件操作工具轻松处理所有文件》在后端开发中,文件操作是一个非常常见但又容易出错的场景,本文小编要向大家介绍一个强大的Go语言文件操作工具库,它能帮你轻松处理各种文件操作场景... 目录为什么需要这个工具?核心功能详解1. 文件/目录存javascript在性检查2. 批量创建目录3. 文件

jvm调优常用命令行工具详解

《jvm调优常用命令行工具详解》:本文主要介绍jvm调优常用命令行工具的用法,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录一 jinfo命令查看参数1.1 查看jvm参数二 jstack命令2.1 查看现场堆栈信息三 jstat 实时查看堆内存,gc情况3.1

C++中函数模板与类模板的简单使用及区别介绍

《C++中函数模板与类模板的简单使用及区别介绍》这篇文章介绍了C++中的模板机制,包括函数模板和类模板的概念、语法和实际应用,函数模板通过类型参数实现泛型操作,而类模板允许创建可处理多种数据类型的类,... 目录一、函数模板定义语法真实示例二、类模板三、关键区别四、注意事项 ‌在C++中,模板是实现泛型编程

Python实现html转png的完美方案介绍

《Python实现html转png的完美方案介绍》这篇文章主要为大家详细介绍了如何使用Python实现html转png功能,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 1.增强稳定性与错误处理建议使用三层异常捕获结构:try: with sync_playwright(

Java使用多线程处理未知任务数的方案介绍

《Java使用多线程处理未知任务数的方案介绍》这篇文章主要为大家详细介绍了Java如何使用多线程实现处理未知任务数,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 知道任务个数,你可以定义好线程数规则,生成线程数去跑代码说明:1.虚拟线程池:使用 Executors.newVir

MySQL使用binlog2sql工具实现在线恢复数据功能

《MySQL使用binlog2sql工具实现在线恢复数据功能》binlog2sql是大众点评开源的一款用于解析MySQLbinlog的工具,根据不同选项,可以得到原始SQL、回滚SQL等,下面我们就来... 目录背景目标步骤准备工作恢复数据结果验证结论背景生产数据库执行 SQL 脚本,一般会经过正规的审批

基于Python开发批量提取Excel图片的小工具

《基于Python开发批量提取Excel图片的小工具》这篇文章主要为大家详细介绍了如何使用Python中的openpyxl库开发一个小工具,可以实现批量提取Excel图片,有需要的小伙伴可以参考一下... 目前有一个需求,就是批量读取当前目录下所有文件夹里的Excel文件,去获取出Excel文件中的图片,并