수학 부분 아직 공식화되지 않았 음/이사벨 위시리스트

Question

수학을 공식화 할 때 현재의 "상태"가 어떨지 궁금합니다. 수학의 특정 영역에서 결과를 증명하는 경향이 있거나, 뭔가 증명하기위한 노력?
공식적인 교정 자료 보관소를 살펴보면 다양한 사람들이 수학의 다양한 부분을 공식화하는 데 열중하고 있지만 좌표 방식이 아니라는 점에서 그럴 것 같지 않습니다. 그냥 호기심).

아직 공식화되지 않았고 현재 위시리스트에서 매우 높은 수학 부분이나 주요 정리가 있습니까? 특히

---

는, (일반) 미분 방정식의 분야에서 너무 많이 수행 된 것으로 보인다 없습니다 -하지만 내 (매우 순진) 인상이 결과를 공식화하는 엡실론 - 델타의 종류부터 devishly 어렵다는 것이다 추론은 종종 형식화에 도움이되지 않습니다. 특히 이미 수학 자체가이 분야에서보다 손쉽게 진행되는 방식으로 이루어지기 때문에 (일반적으로보다 정확하게 대수적으로 쓰여지는 대수학 부분과는 대조적입니다. - 나는 추측한다 - 공식화하기에 덜 지루한 그늘). 이 인상이 맞습니까? 그냥 내 머리 위로 떨어져

Answer 1

:

이

• Freek Wiedijk's list of 100 interesting theorems이 다양한 사람들이 (나를 포함하여) 그 목록에서 정리를 공식화에 노력하고있다,하지만 재미를 위해 대부분이다.
• 또한 HOL Light (대부분 복잡한 분석이지만 토폴로지와 형상)의 결과를 포팅하기위한 노력 (주로 Larry Paulson)이 있습니다.
• Innsbruck의 사람들은 다항식과 관련된 여러 가지 작업을하고 있습니다 (예 : here 참조). 그들이 다시 작성 시스템에서 종료 증거를 위해 그것을 필요로하기 때문에 주로, 나는
• 이를 선택는 '그랜드 이자벨위원회는 정말로 없다

을 확인 공식화 오토마타 및 모델에서 작동 CAVA project이 생각 다음 몇 년 동안 모두가 집중해야 할 수학 영역이지만,이를 어느 정도 독립적으로 수행하는 특정 프로젝트와 그룹이 있습니다.

보통 미분 방정식의 경우 Fabian Immler은 지난 몇 년 동안 많은 것을 수행해 왔습니다. 그는 현재 Lorentz Attractor가 진정으로 혼란 스럽다는 것을 증명하기 위해 노력하고 있습니다. 상당히 복잡한 ODE 관련 자료와 알고리즘이 필요합니다.

ε-δ- 인수가 공식화하기위한 절대적인 공포라고 당신이 맞습니다. 이것이 우리가 그렇게하지 않는 이유입니다. 이자벨의 한도 및 파생물은 필터 (예 : here 참조)과 관련하여 공식화되었으며, 이는 이러한 종류의 추론을 표현하는 매우 우아한 방법입니다.

가지고 좋은 것 것들에 관해서는

하고, 내 지식, 아무도 지금 작업하지 않습니다 :

• 아직 이자벨에
을 수행하지 않은 FREEK Wiedijk의 목록에 거의 아무것도
• 이사벨 (Isabelle)에서 더 추상적 인 대수를 사용하는 것이 좋을 것입니다.(우리가 그 많은 대수학을 가지고 있지 않은 이유 중 하나는 Coq 사람들이 이미 많은 것을 가지고 있기 때문일 것입니다. 의존형으로 이것을 수행하는 것이 더 좋을 수도 있습니다)
• 숫자 이론은별로 없습니다
• 매니 폴드 및 벡터 분석 (분기, 컬, 표면 적분, 등고선 적분)의 이론은
• 내가 분석 조합론의 큰 팬이에요 좋은 것입니다,하지만 난 우리가 점근 적 분석의 종류가 자동화를 두려워 필요한 순간에 부족합니다.

---