人工智能数学验证工具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

相关文章

redis过期key的删除策略介绍

《redis过期key的删除策略介绍》:本文主要介绍redis过期key的删除策略,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录第一种策略:被动删除第二种策略:定期删除第三种策略:强制删除关于big key的清理UNLINK命令FLUSHALL/FLUSHDB命

MySql match against工具详细用法

《MySqlmatchagainst工具详细用法》在MySQL中,MATCH……AGAINST是全文索引(Full-Textindex)的查询语法,它允许你对文本进行高效的全文搜素,支持自然语言搜... 目录一、全文索引的基本概念二、创建全文索引三、自然语言搜索四、布尔搜索五、相关性排序六、全文索引的限制七

Linux内核参数配置与验证详细指南

《Linux内核参数配置与验证详细指南》在Linux系统运维和性能优化中,内核参数(sysctl)的配置至关重要,本文主要来聊聊如何配置与验证这些Linux内核参数,希望对大家有一定的帮助... 目录1. 引言2. 内核参数的作用3. 如何设置内核参数3.1 临时设置(重启失效)3.2 永久设置(重启仍生效

基于Java实现回调监听工具类

《基于Java实现回调监听工具类》这篇文章主要为大家详细介绍了如何基于Java实现一个回调监听工具类,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 目录监听接口类 Listenable实际用法打印结果首先,会用到 函数式接口 Consumer, 通过这个可以解耦回调方法,下面先写一个

使用Python构建一个Hexo博客发布工具

《使用Python构建一个Hexo博客发布工具》虽然Hexo的命令行工具非常强大,但对于日常的博客撰写和发布过程,我总觉得缺少一个直观的图形界面来简化操作,下面我们就来看看如何使用Python构建一个... 目录引言Hexo博客系统简介设计需求技术选择代码实现主框架界面设计核心功能实现1. 发布文章2. 加

JS+HTML实现在线图片水印添加工具

《JS+HTML实现在线图片水印添加工具》在社交媒体和内容创作日益频繁的今天,如何保护原创内容、展示品牌身份成了一个不得不面对的问题,本文将实现一个完全基于HTML+CSS构建的现代化图片水印在线工具... 目录概述功能亮点使用方法技术解析延伸思考运行效果项目源码下载总结概述在社交媒体和内容创作日益频繁的

基于Python打造一个全能文本处理工具

《基于Python打造一个全能文本处理工具》:本文主要介绍一个基于Python+Tkinter开发的全功能本地化文本处理工具,它不仅具备基础的格式转换功能,更集成了中文特色处理等实用功能,有需要的... 目录1. 概述:当文本处理遇上python图形界面2. 功能全景图:六大核心模块解析3.运行效果4. 相

springboot项目中常用的工具类和api详解

《springboot项目中常用的工具类和api详解》在SpringBoot项目中,开发者通常会依赖一些工具类和API来简化开发、提高效率,以下是一些常用的工具类及其典型应用场景,涵盖Spring原生... 目录1. Spring Framework 自带工具类(1) StringUtils(2) Coll

Pytest多环境切换的常见方法介绍

《Pytest多环境切换的常见方法介绍》Pytest作为自动化测试的主力框架,如何实现本地、测试、预发、生产环境的灵活切换,本文总结了通过pytest框架实现自由环境切换的几种方法,大家可以根据需要进... 目录1.pytest-base-url2.hooks函数3.yml和fixture结论你是否也遇到过

基于Python实现高效PPT转图片工具

《基于Python实现高效PPT转图片工具》在日常工作中,PPT是我们常用的演示工具,但有时候我们需要将PPT的内容提取为图片格式以便于展示或保存,所以本文将用Python实现PPT转PNG工具,希望... 目录1. 概述2. 功能使用2.1 安装依赖2.2 使用步骤2.3 代码实现2.4 GUI界面3.效