# 어떤 오류가 사소한 실수인가

> Clean Markdown view of GeekNews topic #14448. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=14448](https://news.hada.io/topic?id=14448)
- GeekNews Markdown: [https://news.hada.io/topic/14448.md](https://news.hada.io/topic/14448.md)
- Type: news
- Author: [chabulhwi](https://news.hada.io/@chabulhwi)
- Published: 2024-04-22T12:13:55+09:00
- Updated: 2024-04-22T12:13:55+09:00
- Original source: [forum.owlofsogang.com](https://forum.owlofsogang.com/t/topic/4689)
- Points: 4
- Comments: 0

## Topic Body

### 어떤 오류가 사소한 실수인가  
  
#### 요점  
  
1. 어떤 정의나 증명에 있는 오류가 고치기 쉽더라도 알아차리기 어렵다면, 그 실수는 사소하지 않습니다.  
1. 어떤 오류는 증명 보조기의 도움을 받아야 찾아낼 수 있습니다.  
  
#### 간추린 본문  
  
* 지난해 12월부터 올해 4월 16일까지 170시간 정도를 들여 [린(Lean) 증명 보조기][lean]의 [표준 라이브러리][std]에 있는 문자열 정리 [`String.splitOn_of_valid`][splitOn_of_valid]를 증명했습니다.  
* 이 정리를 증명하는 도중에 `String.splitOn` 함수의 정의에서 [버그][bug]를 발견했습니다.  
* 이 버그를 고치는 일은 그리 어렵지 않았습니다. 해당 정의에서 `i`를 `i - j`로 바꾸기만 하면 됐어요.  
* 그렇다고 해서 이 오류가 사소한 실수였다고 생각하지는 않습니다. 이 정의에 따르면 `splitOn` 함수가 대개 올바로 작동하지만, 특수한 경우에는 잘못된 결과를 산출하니까요.  
* 린 같은 증명 보조기를 이용하지 않았다면, 이렇게 미묘한 오류를 저는 절대로 못 찾아냈을 것입니다.  
  
[lean]: https://lean-lang.org/  
[std]: https://github.com/leanprover/std4  
[splitOn_of_valid]: https://github.com/leanprover/std4/pull/743/files#diff-b2fb96bb7d0273dbe3a81a67bb9b432c089139ac50e3e0b3578f40cac0de2a51R627-R636  
[bug]: https://github.com/leanprover/lean4/issues/3829

## Comments



_No public comments on this page._